2IMF00 --- Seminar Formal System Analysis (2019-2020)

In 2019/2020 this seminar will be held in quartile 2, the first meeting will be on Monday, November 11, 2019. 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 (2018/19) or this page (before 2018).


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 12, 2019, and together they decide about the topic to be investigated. These topics will be briefly presented/discussed on the first meeting on Monday, November 11. The supervision will be mainly done by the staff member proposing the assignment. 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 13, 2019, the students communicate the choice they have made and the research question(s) they will address in a 5-minute (powerpoint) presentation. Guidelines will be discussed during the first lecture
  • 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 technical 'mid-term' 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 5, 2020.
  • This version will be considered by two other students who have to provide a one-page review on this report within one week, so no later than January 12, 2020.
  • All students are expected to be present at all presentations, and participate in discussions.


Schedule (tentative from 13 November onwards; will be discussed on second meeting)
  • 11 Nov: 1st meeting (Fenix 0.144; 13.30-14.15)
  • 13 Nov: 5 minute presentations (MF 14; 9.45-10.30)
  • 16 Dec: 20 minute presentations (Fenix; 13.30-15.15). Notes on writing report/review can be downloaded here
  • 05 Jan: hand in report via email
  • 12 Jan: hand in reviews
  • 19 Jan: 40 minute presentations (Fenix 0.144; 13.30-15.15)
  • 21 Jan: 40 minute presentations (MF 14; 8.45-10.30)
  • 26 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.ir. Jeroen Keiren, email: j.j.a.keiren@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) Featured transition systems are an extension of standared labeled transition systems to specifically deal with behavior-oriented modeling of software product lines (SPL), see e.g. [1,2]. In a
    recently completed master thesis [3] an algorithm is proposed to decide the model checking problem for SPL and applied to the SPL reference examples of the minepump and the elevator. Goal of this seminar assignment is to apply the approach mentioned to the case of the vending machine [1] and the coffee machine of [4], where the latter is an example of an SPL with a more complex feature diagram.

    [1] A. Classen, P. Heymans, P.-Y. Schobbens, A. Legay and J.-F. Raskin, Model checking lots of systems: Efficient verification of temporal properties in software product lines, Proc. ICSE'10, ACM 2010, pp. 335--344
    [2] M.H. ter Beek, E.P. de Vink and T.A.C. Willemse, Family-Based Model Checking with mCRL2, Proc. FASE'17, LNCS, 2017, pp. 387--405
    [3] S. van Loo, Verifying featured transition systems using variability parity games, Eindhoven University of Technology 2019
    [4] M.H. ter Beek and E.P. de Vink, Using mCRL2 for the Analysis of Software Product Lines, Proc. FormaliSE'14, IEEE 2014, pp. 31--37

  • (Keiren) Refining our confidence in refinable partition data structures.
    Efficient algorithms for behavioural equivalences such as stuttering bisimulation and branching bisimulation rely on refinable partition data structures [1]. We recently developed an O(m log n) algorithm for computing branching bisimulation equivalence of labelled transition systems [2], and implemented it in the mCRL2 toolset. Since the proofs of correctness and of the time complexity of the algorithm are highly non-trivial, it is desired to formally verify these proofs. As a stepping stone towards the full verification of the algorithm, in this project you formalise the refinable partition data structures used in the algorithm. For this, you use one of the theorem provers Coq or Isabelle. You also identify and prove some of the properties that the branching bisimulation algorithm requires to hold in the correctness or complexity arguments.

    [1] Valmari, A., Lehtinen, P.: Efficient Minimization of DFAs with Partial Transition Functions. In: Albers, S. and Weil, P. (eds.) STACS. pp. 645–656 Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany (2008).
    [2] Jansen, D.N. et al.: A simpler O(m log n) algorithm for branching bisimilarity on labelled transition systems. (2019).

  • (Keiren) Should we preprocess parity games using stuttering bisimulation?
    The model checking problem can be translated into parity games. In the past, several equivalences on parity games have been studied, based on behavioural equivalences from the domain of process theory. In particular, we showed that parity games can be reduced using stuttering bisimulation while preserving the solution. Whether it is actually useful in practice to preprocess a parity game using stuttering bisimulation is not so clear. In our original work [1] we performed experiments that indicate that it is useful to do this preprocessing. However, advances in the implementations of parity game solvers tipped the scales in the other direction, leading me to conclude in my PhD thesis that this preprocessing is generally unwise [2].
    Recently, however, the complexity of the algorithm for stuttering bisimulation equivalence for Kripke structures has been improved from O(mn) to O(m log n), where m is the number of transitions and n is the number of states in a Kripke structure [3]. This improved algorithm has been implemented in the mCRL2 toolset. Additionally, there have been several improvements in the state of the art of parity game solving, using new algorithms and new implementations. A particularly fast parity game solver is Oink [4].
    In this assignment, the O(m log n) algorithm for Kripke structures in the mCRL2 toolset should be adapted to allow reducing parity games. Furthermore, the experiments from [2] should be redone using this new implementation, and using the fastest parity game solvers that are currently available. This should ultimately lead to a recommendation whether we should preprocess parity games using stuttering bisimulation prior to solving or not.

    [1] Cranen, S. et al.: Stuttering Mostly Speeds Up Solving Parity Games. In: Bobaru, M. et al. (eds.) NFM. pp. 207-221 Springer, Berlin, Heidelberg (2011).
    [2] Keiren, J.J.A.: Advanced reduction techniques for model checking. Eindhoven University of Technology (2013).  (Chapter 5)
    [3] Groote, J.F. et al.: An O(m log n) algorithm for computing stuttering equivalence and branching bisimulation. ACM Trans. Comput. Logic. 18, 2, 13:1-13:34 (2017).
    [4] van Dijk, T.: Oink: An Implementation and Evaluation of Modern Parity Game Solvers. In: Beyer, D. and Huisman, M. (eds.) TACAS. pp. 291-308 Springer International Publishing, Cham (2018).

  • (Keiren) When are xMAS networks well-formed?
    xMAS [1] is a language that can be used to give a high-level description of hardware components. It consists of microarchitectural primitives such as queues. In a hardware design, such primitives are connected by channels. On a high level, we want to reason about components and channels, and verify whether a hardware design satisfies a given specification using, e.g., model checking [2,3]. For this, we need to understand the low level semantics of a network. One of the characteristics of this low-level semantics is that a high-level channel actually consists of three separate signals, indicating whether the source of the data is ready to transmit, the target is ready to receive, and one containing the actual data. The network is only well-defined if, on this low level, the design does not contain combinatorial cycles. So, even if we design a system on the high level we need to be aware of what happens on the low level. In this assignment, it should be investigated whether design criteria on the high level can be given that guarantees absence of combinatorial cycles on the lower level.

    [1] Chatterjee, S. et al.: xMAS: quick formal modeling of communication fabrics to enable verification. IEEE Design Test of Computers. 29, 3, 80-88 (2012).
    [2] Chatterjee, S., Kishinevsky, M.: Automatic generation of inductive invariants from high-level microarchitectural models of communication fabrics. Form Methods Syst Des. 40, 2, 147-169 (2012).
    [3] Gotmanov, A. et al.: Verifying deadlock-freedom of communication fabrics. In: VMCAI. pp. 214-231 Springer (2011).

  • (Luttik) Reliable communication in Railway Signalling Systems
    The RaSTA (Rail Safe Transport Application) protocol is a networking protocol that serves as a safety and retransmission layer in the networking stack. RaSTA is developed by and for the railway industry. It will be used for the communication between various railway infrastructure elements (e.g., points, signals, level crossings, etc.) and the interlocking (the device that ensures that only safe routes can be set between two signals). RaSTA is similar to TCP but has stricter timing requirements, the connection is monitored with so-called heart beat messages, and timeouts deliberately cause disconnects. The goal of the assignment is to model and verify the RaSTA protocol using the mCRL2 toolset, focussing on railway-specific safety aspects.

  • (Luttik) Model-checking non-atomic (group) mutual exclusion algorithms
    Some of the well-known mutual exclusion algorithms (e.g., Peterson’s mutual exclusion algorithm) rely on atomicity of reading and writing to shared memory. There also exist mutual exclusion algorithms that do not rely on such assumptions. The goal would be to verify the correctness of one or more of such algorithms, and in particular then also consider their tolerance to non-atomicity. Generalisations to more than 2 processes, group mutual exclusion, and justness assumptions can also be considered.

  • (Lutttik/Willemse) mCRL2 with global variables
    The process specification language mCRL2 does not have a notion of global variable; parallel components  can only communicate by message passing. For many applications, especially when mCRL2 specifications are obtained through translation from another formalism that does have global variables, their absence in mCRL2 is inconvenient. The assignment is to investigate how a notion of global variable can be added to mCRL2, and what would be the theoretical and practical implications of such an addition. The following questions could be addressed: What are the implications for the process-algebraic semantics of mCRL2 specifications? What are appropriate notions of behavioural equivalence? How should global variables be used in modal logics for specifying properties of mCRL2 specifications? How would adding a notion of global variable to mCRL2 affect the tools in the mCRL2 toolset.


  • (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) Fair Testing Preorder
    Behavioural preorders have application in a step-wise software development methodology. In such a methodology, a formal, behavioural specification of a system is refined into an implementation in a step-wise manner. There are many refinement theories; popular ones include the stable failures refinement and the failures-divergence refinement [1] prominently used in the CSP process algebra, but also in industry (e.g. in the Dezyne language, developed by Verum Software Tools, B.V. in the Eindhoven region). Most refinement relations deal with divergences either by ignoring these or by considering these as catastrophic. The refinement relation called Fair Testing [2], however, treats divergences in a special way, allowing for some room of fairness in 'exiting' a divergent computation. The assignment is to study the Fair Testing preorder, compare it to the aforementioned preorders and, e.g., the Impossible Futures relation, or to study the algorithm for deciding the fair testing preorder.

    [1] M. Laveaux, J.F. Groote and T.A.C. Willemse: Correct and Efficient Antichain Algorithms for Refinement Checking. FORTE 2019: 185-203
    [2] Arend Rensink and Walter Vogler: Fair testing. Inf. Comput. 205(2): 125-198 (2007)


  • (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.