2IMF00 --- Seminar Formal System Analysis

In 2018/2019 this seminar will be held in quartile 2, the first meeting will be on Monday, November 12, 2018. Supervisor: Dr.ir. T.A.C. Willemse, Metaforum 6.073, tel 2999, t.a.c.willemse@tue.nl. For previous incarnations of this course, see this page.


Goal/contents

In this seminar, a group of master students will conduct research in the field of formal system analysis, i.e. the study of formalisms (e.g. their syntax, semantics and/or algorithmics) and their use in specifying, analysis and/or verifying (software) systems, as a preparation to the master's project. This will be done in the following ways:
  • Every student chooses a topic from the list of topics proposed by researchers in the group, and contacts the group member who proposed it, no later than Tuesday, November 13, 2018, and together they decide about the topic to be investigated. Provided that sufficiently many students enrolled, most of these topics will be presented on the first meeting on Monday, November 12. The supervision will be mainly done by the respective group member. You can also propose your own topic after consultation with, and agreement of an FSA supervisor; if you have a topic in mind for which no supervisor is obvious, please contact the coordinator.
  • In the meeting of Wednesday, November 14, 2018, the students communicate the choice they have made and the research question(s) they will address in a 5-minute presentation.
  • Research papers and/or book chapters will be studied and presented by the students, with a focus on research questions.
  • Examples related to the presented material or other investigations will be elaborated. If suitable, experiments related to these examples will be executed, either by using existing implementations or by developing ad hoc implementation.
  • Every student will give a first presentation of 20 minutes and a final presentation of 45 minutes.
  • Conclusions of the investigations are presented in a report. This report has the format of a paper with introduction, conclusions and bibliography, has a size of at most 40 pages, but preferrably much less. A first version should be handed in no later than January 6, 2019.
  • This version will be considered by two other students which have to provide a one-page review on this report within one week, so no later than January 13, 2019.
  • All students are present at all presentations, and participate in discussions.


Schedule
  • 12 Nov: 1st meeting (MF 6.073)
  • 14 Nov: 5 minute presentations (TRAVERSE 3; 9.45-10.30)
  • 10 Dec: 20 minute presentations (TAVERSE 3; 13.30-15.15). Notes on writing report/review can be downloaded here
  • 06 Jan: hand in report via email
  • 13 Jan: hand in reviews
  • 16 Jan: 45 minute presentations (TRAVERSE 3; 8.45-10.30)
  • 28 Jan: hand in final report via email


Guidelines for grading

The final grade is mainly established on the basis of the following ingredients:
  • The quality and contents of the presentations,
  • The quality and contents of the report,
  • The process of dealing with the topic, the initiatives taken and the amount of supervision required,
  • The quality of the review(s),
  • The level of participation in all meetings.


Staff members

dr. Erik de Vink, email: e.p.d.vink@tue.nl
dr. Bas Luttik, email: s.p.luttik@tue.nl
dr.ir Wieger Wesselink, email: j.w.wesselink@tue.nl
dr.ir Tim Willemse, email: t.a.c.willemse@tue.nl
prof.dr. Herman Geuvers, email: herman@cs.ru.nl
prof.dr.ir. Jan Friso Groote, email: j.f.groote@tue.nl
prof.dr. Hans Zantema, email: h.zantema@tue.nl


Assignments

Participants can choose freely among the following problem descriptions:
  • (De Vink) Applying tau-Confluence in Paradigm model analysis
    The lpsconfcheck tool in the mCRL2 toolset seeks to exploit an advanced technique called tau-confluency analysis [1]. If applicable state spaces can be significantly be reduced and subsequently speed up verification substantially. The coordination modelling language Paradigm is a component-based interaction language that translates into mCRL2 [2]. The Paradigm language distinguishes global inter-component interaction and local inner-component behavior. Goal of the project is to investigate to what extent tau-confluency is guaranteed by a Paradigm model and how the technique can be used advantageously for the analysis of Paradigm models.

    [1] Jan Friso Groote and Jaco van de Pol, State Space Reduction Using Partial tau-Confluence. Proc. MFCS 2000, p383-393 (2000)
    [2] Suzana Andova, Luuk Groenewegen and Erik de Vink, Dynamic Consistency in Process Algebra: From Paradigm to ACP. ENTCS 229(2), p3-20 (2009)

  • (Groote) Verification of the correctness of rewrite rules for n-bit calculations for natural numbers.
    In order to increase the speed of number calculations in the mCRL2 toolset there is a proposal to replace the @cDub/@c0 based natural numbers by the 64 bit natural numbers that are native to modern processors. This leads to a set of rather complex rewrite rules to calculate operations such as multiplication, addition, modulo, division and the square root.  The correctness has been shown by a high level proof, and by extensive test runs. The question is whether we can prove the correctness of the rules beyond any doubt, using a proof checker such as Coq or PVS. This would add enormously to the trustworthiness of the rules.

  • (Wesselink) Compositional verification of large UML models
    Recently in the context of an OPZuid project an automated translation from UML models provided by the company Cordis Automation to mCRL2 has been developed. These are hierarchical models, where state machines are used for the control of the components. The execution of the models is entirely sequential. Real life models made by their customers tend to be quite large. Even after applying several abstractions to the models, mCRL2 can only verify sub-components of limited size.

    A possible approach to deal with this problem is to separately generate state spaces for sub-components, minimize them, and compose them into a state space for a larger model. The goal of this assignment is to do a literature study for existing work in this direction, and to study how well these techniques can be applied in the given context. Typical interaction between components consists of reading and writing state variables of sub-components, inspecting the current state of a state machine in a sub-component, and scheduling a command that is executed by a sub-component as soon as it gets a window of execution.

  • (Willemse) Satisfiability of (fragments of) the first-order modal mu-calculus
    The modal mu-calculus can be used for formalising requirements of systems, and verifying whether such systems then meet such requirements can be done by means of model checking. The first-order extension of the modal mu-calculus adds facilities to permit reasoning about data in such requirements. However, writing a (sensible) formula in the (first-order) modal mu-calculus is not trivial. To aid users in better understanding the formulae they write, one can (automatically) generate a model, if it exists, in which the formula holds. The proposed assignment is to study algorithms and techniques found in the literature for this problem for (fragments of) the modal mu-calculus, implement a good candidate algorithm and investigate whether it can be extended to deal with a larger fragment of the first-order modal mu-calculus.

  • (Zantema) Learning automata by SAT solving
    We consider the issue of finding an automaton (DFA, NFA) satisfying a given set of constraints. These constraints can be of the shape that particular strings should or should not be accepted by the automaton, but can also involve properties of the accepting language or behavioral properties in considering the automaton as a transition system. In this project it will be investigated, based on some initial literature, how SAT/SMT solving may serve for solving this problem.
    As an alternative seminar project also other problems may be considered to exploit SAT/SMT solvers, like scheduling problems.