Seminar Formal System Analysis (2IMF00)

List of topics for 2017/2018

Jan Friso Groote MF 6.079b, j.f.groote@TUE.nl

Topic: Modal formulas to PBES
A modal formula is transformed into a PBES. This PBES contains quantifiers. In general it is useful when the quantifiers can be pushed as much as possible inside the pbes. In particular it is useful when it can be moved inside equations. An example is
mu X = exists n:Nat.Y(n)
mu Y(m:Nat)= (m==2) || Y(m)
We derive
X = exists n:Nat.Y(n) = exists n:Nat n==2 || Y(n) = exists n:Nat n==2 || exists n:Nat Y(n) = true || X.
So, it is now easy to derive that X=true. The question is whether an algorithm can be devised that can do this in general. This algorithm would be very useful in the tools, as people often write quantifiers in front of their modal formulas, often making life much harder for the verification tools.

Topic: Data types to SMT
It is possible to write abstract data types in mCRL2. In order to systematically prove properties about them it would be useful to come up with a generic transformation scheme to the input of SMT solvers. For instance the built in data types such as Real, Int and Nat can be mapped to built in data types of SMT solvers. Enumerated datatypes can be translated to constructors inside the language. The goal is then to evaluate expression of type Bool, and determine whether these are equal to true or false.

Bas Luttik MF 6.072, s.p.luttik@tue.nl

Topic: Modelling and analysing fixed virtual blocks in mCRL2
Railway companies are in the process of rolling out a new standardised railway signalling system, called ERTMS, that should facilitate the safe movement of trains across borders within Europe and at the same time increase the capacity of the existing infrastructure. Currently, tracks are divided up into fixed blocks, and signalling principles are supposed to prevent that two trains end up on the same block. Capacity improvement by adopting ERTMS is, in particular, expected from the introduction of so-called virtual blocks. There are still significant technological difficulties to be overcome before the concept of virtual block can be implemented safely. Railway companies and suppliers of railway equipment are, therefore, experimenting with the concept of fixed virtual blocks, which should give some of the advantages of virtual blocks without all the technological difficulties.
There is a document that describes the requirements of hybrid ERTMS level 3, which includes fixed virtual blocks. The goal of the assignment is to model and analyse these requirements in mCRL2.

Topic: Adding sequential composition to the axiomatisations of van Glabbeek's spectrum.
For all behavioural equivalences in van Glabbeek's linear time - branching time spectrum it is known whether there exists a finite axiomatisation in the context of the language BCCSP (which has a constant 0, unary action prefixes a. and a binary operation + for choice). In [1], an overview of these results is presented. It would be interesting to investigate what is the effect of adding operations such as sequential composition, parallel composition, ... on the existence of finite axiomatisations.
For some behavioural equivalences in the spectrum it will be reasonably straightforward to extend the existing finite axiomatisation for BCCSP with sequential composition, or to prove that the non-existence of a finite axiomatisation still holds true if sequential composition is added. For some others it will be harder. The assignment would be to make a start with considering the spectrum in the context of a language with sequential composition.
Reference: [1] Taolue Chen, Wan Fokkink, Bas Luttik, and Sumit Nain. On finite alphabets and infinite bases. Information and Computation 206(5):492-519, 2008.

Topic: Axiomatising sequential composition
In [1], an revised operational semantics for sequential composition in the context of intermediate termination was proposed. The goal of this seminar assignment is to find a sound and ground-complete set of axioms for TSP modulo (strong) bisimilarity.
[1] Jos Baeten, Bas Luttik and Fei Yang. Sequential Composition in the Presence of Intermediate Termination (Extended Abstract). Proceedings of EXPRESS/SOS 2017, EPTCS 255, 2017, pp. 1-17. (Available at http://eptcs.web.cse.unsw.edu.au/paper.cgi?EXPRESSSOS2017.1.pdf.)

Bas Luttik MF 6.072, s.p.luttik@tue.nl, and Tim Willemse MF 6.073, t.a.c.willemse@tue.nl

Topic: Can mCRL2 analyse mutual exclusion?
In recent work by van Glabbeek and Hofner [1] it is argued that standard process algebras such as the process algebras discussed in 2IMF10, and also the process algebra underly mCRL2, are fundamentally insufficiently expressive to analyse mutual exclusion protocols. This contradicts a common belief that, on a certain level of abstraction, process algebraic formalisms are sufficiently expressive for the analysis of any distributed system. In follow-up work [2], Dyseryn, van Glabbeek and Hofner show that extending process algebras with signals upgrades their capability sufficiently to facilitate the analysis of mutual exclusion protocols.
The specification language mCRL2 includes an extra feature compared to standard process algebras that has not explicitly been considered in the aforementioned works: multi-actions. Especially in combination with data, it may (or may not!) be that mCRL2 is sufficiently expressive to specify and analyse mutual exclusion protocols.
The goal of this seminar assignment is to determine to which extent the arguments in [1] also go through for the process-algebraic specification language mCRL2, in particular considering the role of multi-actions. Can multi-actions perhaps be used to specify Peterson.s mutual exclusion algorithm accurately and prove it correct? This seminar assignment may (but does not have to) prepare for an MSc thesis project on signals and global variables in mCRL2.
[1] Rob van Glabbeek and Peter Hofner. CCS: It.s not Fair! Fair Schedulers cannot be implemented in CCS-like languages. Acta Informatica 52(2-3), 2015, pp. 175-205. (Available at http://theory.stanford.edu/~rvg/abstracts.html#107.)
[2] Victor Dyseryn, Rob van Glabbeek and Peter Hofner. Analysing Mutual Exclusion Using Process Algebra with Signals. Proceedings of EXPRESS/SOS 2017, EPTCS 255, 2017, pp. 18-34. (Available at http://eptcs.web.cse.unsw.edu.au/paper.cgi?EXPRESSSOS2017.2.pdf.)

Topic: Explicit Divergence in Weak Bisimulation
Branching bisimilarity and weak bisimilarity are typically used in process algebras where silent steps are used to abstract from internal behaviours. This facilitates relating implementations and specifications. For branching bisimilarity, there is a natural notion of sensitivity to divergence (i.e. infinite internal activity), and there are a number of ways in which branching bisimilarity with explicit divergence can be characterised: relationally, through coloured traces, or through an appropriate modal logic. For weak bisimilarity, the case is less clear; that is, it is not clear what the natural notion of divergence sensitivity is in the context of weak bisimilarity. This assignment deals with investigating divergence aware extensions of the relational characterisation of weak bisimilarity and, time permitting, linking these to an appropriate modal logic.

Topic: 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. It would therefore be interesting 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 assignment would consist of addressing some of the following questions: What are the implications for the process-algebraic semantics of mCRL2 specifications? What are the 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.
Starting point for this research would be the paper "Process Algebra with Propositional Signals" by Jan A. Bergstra and Jos C. M. Baeten, Theoretical Computer Science 177(2):381-405, 1997.

Tim Willemse MF 6.073, t.a.c.willemse@tue.nl

Topic: BDD-based Parity Game Solving
Parity games provide an operational, game-based interpretation for problems such as model checking and equivalence checking. Many algorithms for solving parity games have been proposed and several implementations have found their way in cutting-edge verification tool sets. These implementations typically assume a parity game is given explicitly as a graph. Since the graphs in the context of model checking can become prohibitively large, techniques such as Binary Decision Diagrams for representing sets of vertices and edges may be required to deal with this complexity. It is not clear from the outset which of the parity game solving algorithms can be easily modified to take advantage of a BDD representation. The assignment is thus a quest to find out which parity game solving algorithms can be made to work efficiently with BDDs.

Erik de Vink MF 6.075, e.p.d.vink@tue.nl

(Due to a sabbatical, this year Erik de Vink is not avialable as a supervisor)

Julien Schmaltz MF 6.071b, j.schmaltz@tue.nl

Topic: Counter-example guided invariant generation
In this project, you will investigate the feasibility of generating invariants based on counter-examples. Our current liveness checker relies on SMT solving and an overapproximation of the state space. It is sound in the sense that it correctly returns "live" results but it is incomplete in the sense that it sometimes returns "not live" for live systems. The objective of this project is to study the generation of invariants from the negation of these counter-examples. The work for this project involves building a prototype for the invariant generator and conducting experiments. Challenges include (1) extraction of possible invariants from the counter-examples and (2) optimisations to speed-up the invariant generation.

MaDL is our DSL for high-level modelling. It is a continuation of work started with Intel and their xMAS language. We recently added state machines to MaDL making it also suitable to model control structures. In this project, you will investigate code generation for MaDL. The objective is to generate C/C++ (or any language you like) from MaDL specifications. The project can either be theoretical and focus on the challenge to define and ensure a correctness relation between the MaDL and the generated code; or be practical and focus on the challenges related to code generation (efficiency or even looking at multi-threaded code).

Hans Zantema, MF 6.078, h.zantema@tue.nl

Topic: Automatic concept generation
The company Punch Powertrain develops parts of cars. They want to find automatically all solutions for sets of requirements on a sequence of components. Attempts to do this by Prolog easily ran out of resources. Some first experiments to use a SAT/SMT solver instead look promising. The underlying problem is finding a graph of which every node is of some type, and every type of nodes has a fixed degree, and there are restrictions on connections between different types. One challenge is symmetry reduction: describe the graphs in such a way that essentially the same solutions are not counted twice. The project is to elaborate this further, and to figure out to which order of magnitude this is feasible to be solved by SAT/SMT.

Topic: 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.

Anton Wijs, MF 6.077, a.j.wijs@tue.nl, and Sander de Putter, S.M.J.d.Putter@tue.nl

Topic: Applying machine learning to evaluate compositional model checking
To combat state space explosion several compositional verification approaches have been proposed. Thorough evaluation of these approaches are rarely reported in the literature. An evaluation of assume-guarantee reasoning was recently conducted in [1]. The study raises doubt whether assume-guarantee reasoning is useful as an effective alternative to the classical monolithic verification. An alternative approach is compositional aggregation that attempted to limit state space explosion during the parallel composition of concurrent components with intermediate minimisation. However, evaluation has been limited to small benchmarks. In this project you will apply machine learning techniques to develop a heuristic for evaluating whether compositional aggregation may be efficient for a given model.
[1] Cobleigh, J.M., Avrunin, G.S., Clarke, L.A.: Breaking up is hard to do: An evaluation of automated assume-guarantee reasoning. ACM Trans. Softw. Eng. Methodol. 17(2), 7:1.7:52 (May 2008)

Topic: Verify whether partial models satisfy partial properties
In model-driven development, systems are often incrementally designed, meaning that functional details about the system are introduced in a number of steps. In such a workflow, formal verification could be particularly effective if the used technique can handle the fact that parts of the current system design and/or property to be checked are currently not well-specified. Then, at a later stage when some of those gaps have been filled, ideally, the technique can reuse earlier results to efficiently determine whether the more concrete system still satisfies the more concrete property. Several approaches to handle partial state spaces and partial properties have been suggested in the literature.
In the last few years, we have developed a verification technique to verify whether model transformations, formalised as LTS transformations, preserve particular functional properties. The next step is to determine whether a transformation applicable on both systems and properties is guaranteed to produce new systems that satisfy the accompanying new properties. This would allow for the maintenance of properties, instead of leaving them the way they are initially specified. Ideas from the work on partial state spaces may be applicable in this context as well, but this is currently not known. The assignment is to conduct a literature study to investigate the current state-of-the-art in the verification of partially specified systems using partially specified properties, with the aim to determine to what extent the findings are applicable on the verification of transformations. If desired, this assignment could be extended to a master thesis assignment, by subsequently working on the verification of transformations that transform both systems and properties.

Topic: Accelerating model checking with Graphics Processors using CUDA 9.0
Since 2014, we have been investigating the possibilities to perform model checking, which is computationally very intensive, on graphics processors (GPUs). Initially designed specifically for graphical tasks, these days, GPUs are general purpose, and GPU programs can be written similar to how standard programs are implemented. We target the GPUs developed by NVIDIA, for which the CUDA programming language can be used, which extends C and C++ with some additional constructs. Over the years, the resulting model checker, called GPUexplore, has been optimised, to the current point at which it can be 500 times faster than a traditional, single-core CPU-based model checker. Very recently, a new version of CUDA has been released, which provides, among other features, a new powerful feature called cooperative groups. We believe that with this feature, there is real potential to further improve the performance of GPUexplore, but this remains to be investigated. The assignment is to study this new feature, understand the inner workings of GPUexplore, and experiment with the new capabilities of CUDA 9 to improve GPUexplore.s performance.

Last change: November 3, 2017