2IMF00
--- Seminar Formal System
Analysis (2018-2019)
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. 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
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.