Interested in formal verification of critical systems (targeting SIL-3 and -4) ? This topic looks at Railway infrastructure designs, together with the industry partner RailComplete AS. The topic involves the use of the successful tool iSAT for verifying safety properties for a case study that RailComplete works with.
The student will learn to use the verification tool iSAT and how to model hybrid systems. The project may include software development to integrate the iSAT tools set into the framework of RailComplete.
You may be spending time in the RailComplete company, which designs railway infrastructures such as rail track designs or complete railway stations.
The particular difficulty with safety-critical systems is that they are combining controller components, having discrete behaviour, with physical components, having continuous behaviour. This makes safety-critical systems part of what is more generally called cyber-physical systems since the controllers are usually computerized.
As learning outcomes, the student will learn to work with the formal tool set iSAT and will learn how to model safety critical systems which are of a hybrid nature, i.e., involve both continuous and discrete behaviours. For modelling hybrid systems it is good if the student is inclined towards learning some needed mathematics, like differential algebraic equations and SAT solving.
The practical part of the topic can also be more towards implementation, and look at how the iSAT tools can be integrated in the software that RailComplete uses. This involves looking at coupling/translations between the input languages of the different software. This could also involve working with finding good translation methods between the informal rules that govern railway designs, and the input language of the formal tool.
For mastering the iSAT tools there could be possibilities for visits abroad to eg. Germany in the group in Oldenburg actively developing iSAT. (Such visits, possibly to other places, are usually discussed during the master project, depending on the actual direction taken and on the motivation of the student.)