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.
Topic: Code generation for xMAS/MaDL.
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