Master thesis assignments
Below you find a number of examples of potential assignments for a master thesis. In general there are far more assignments than can
be listed here. It is always more fruitful to do a master thesis assignment that matches your interests. Therefore, I invite you
to discuss your particular desires with me. Please note that it is wise to at least start with organizing your master thesis two
months in advance. Students in Embedded Systems that first have to do a premaster assignment should contact me well before. Doing
the premaster assignment beside other courses in part time is very well possible.
If you visit me to discuss potential master thesis assignments, I appreciate if you can bring a list of attended courses.
Having completed a fair share of the courses of the Formal System Analysis group
(System Validation, Algorithms for Model Checking, Process Algebra, Automated Reasoning, Proving with
Computer Assistance) is very desirable to successfully complete your master assignment.
Verification of the correctness of Programmable Logical Controllers at Vitens.
Vitens is the largest company providing drinking water in the Netherlands,
supplying over one third of the Dutch population. The supply of
drinking water is an essential commodity and as such it must always
be available. Therefore, the software infrastructure must satisfy the
highest standards of quality. In order to improve the standards further,
and reduce the costs and efforts of software maintenance, Vitens wants to
employ software verification techniques and cooperate with universities
to include science in these matters.
In particular it wants to use satisfiability methods to verify the correctness of
their infrastructure of Programmable Logical Controllers.
The question for this assignment is whether satisfiability techniques
are applicable in the context of the software infrastructure of Vitens.
This assignment consists of building a translator from Vitens PLC code
for one or two specific drinking water plants (to be determined), to
propositional formulas, identify together with the software engineers
at Vitens which requirements must be satisfied and prove that these
requirements are valid for all conceivable runs of the software at
A large part of the work will be carried out at Vitens in Arnhem.
At TATA steel IJmuiden
IJmuiden several programming departments are responsible
for maintaining the control software for the heavy equipment required to make steel.
Many of these systems are controlled by Programmable Logic Controllers. A
careful testing process is in place to guarantee that the control software does not
cause the equipment to malfunction.
The programming departments are interested in cutting down the testing costs by
applying formal techniques, especially satisfiability techniques. To investigate this
a translator must be made from PLC code to propositional logic formulas. Furthermore,
in cooperation with the software engineers at Tata steel, requirements on the software
must be formulated that can subsequently be verified.
Kandidates for this assignment must have a good skills in programming, program transformation and logic.
They must have finished the course Automated Reasoning with good results.
in Best software is being redesigned continuously. Currently, this is done using model based design using
the languages ASD and Dezyne developed at Verum. An interesting question is whether the
newly designed software behaves exactly as the original software. It appears that model based testing is the excellent
way to go ahead, where the old software is tested for compliance with the new models. The research question is to
see whether this is viable by applying model based testing on a recently renewed piece of software.
Modelling and analysing systems with hard real time constraints is hard. At
ASML, where large parts of the software is currently designed using model driven design,
there is a desire to be able to model and analyse systems where hard real time constraints play a role. Such requirements
vary from input signals that must be processed within a particular time interval, robot arms that must have moved out of a
critical region within a certain time, to wafers that must have been processed in time. There are various methods and tools
available to do such analyses, but the question is whether such methods will be able to provide concrete insights in
concrete real time systems. Your assignment will be to model concrete real time behaviour of concrete systems at ASML and
see which methods are most effective in proving that those systems satisfy the required real time properties.
Probabilistic behaviour is very interesting. This is the reason that the mCRL2 toolset supports probabilities. Checking
probabilistic modal formulas is a challenging endeavour of which the basic techniques to do so are known. This master
assignment is about making the available theory concrete in a tool. The basic steps are to define the basic modal property
language and to define the translation towards PRESs, the probabilistic counterpart of PBESs. If there is sufficient time
available, an algorithm to solve the PRESs is also very desirable.
Plain probabilistic bisimulation is provided with a very efficient algorithms to calculate whether two states are equal.
The situation is different when combined transitions are also allowed. If there are two nondeterministic transitions
a.s and a.t, then a combined transition is a.(p s+(1-p) t), or in words, after the action a, state s can be reached with probablity
p and state t can be reached with probability (1-p). Combined probabilistic bisimulation takes such combined transitions into
account. The question is whether an efficient algorithm can be found and implemented that determines whether two states are
combined probabilistically bisimilar.
Return to the homepage of the Formal System Analysis group.
Return to the homepage of J.F. Groote.