Ruud Meeuws: Model Checking Supermodels Workbench with mCRL2
At Sioux, a model-driven development tool is created. It allows users to create a model and generate software for specific hardware platforms. For this tool, Sioux wants to incorporate model checking in order to improve the correctness and safety of software. To see whether model checking is viable for industrial models, we want to explore …continue reading
Mark Bouwman: A model-based test platform for rail signalling systems
As technology progresses, newer, and more complex, solutions are employed to verify that rail signalling systems are safe. Formal methods provide ways to increase rigour in the verification process. This precision, accompanied by the ongoing increase of computational power of computers, also opens up ways to partially automate parts of the verification process. We present …continue reading
Hong Zhang: Quality metrics for ASOME data models
At ASML the ASOME data modelling language has been defined. Many system designers are defining models in this language, and the question is whether there is an easy way to assess that these models are ok. This can be done using metrics. The question is which metrics are proper. In this MSc research various metrics …continue reading
Ferry Timmers: A complete axiomatisation for probabilistic trace equivalence
In the thesis a complete axiomatisation is given for probabilistic trace equivalence for finite
processes. The axiomatisation is remarkably complex, which may explain that nobody formulated
such a complete axiomatisation yet.
Lisette Sanchez: Learning software behavior through active automata learning with data
The topic of the thesis is find out whether the LS* learning algorithm, that can learn register automata with abstract data parameters from actual software is practically applicable in an industrial context. The algorithm can for instance learn a queue with limited size that stores arbitrary natural numbers. The conclusion is that indeed practical software …continue reading
Lois Nijland: Adding sequential composition and termination to the linear time – branching time spectrum
Van Glabbeek presented the linear time – branching time spectrum of behavioural semantics and gave sound, ground-complete axiomatisations for the process theory BCCSP. Groote and Chen et al. proved for the semantics in the spectrum whether there exist finite axiomatisations that are omega-complete. We add termination and sequential composition to the spectrum by studying the …continue reading
Astrid Belder: Decidability of bisimilarity and axiomatisation for sequential processes in the presence of intermediate termination
An alternative semantics for sequential composition in a setting with intermediate termination was proposed in a recent article by Baeten, Luttik and Yang. We consider two open questions regarding sequential processes with intermediate termination that use the revised semantics for sequential composition (TSP;). First, a ground-complete axiomatisation is proposed for TSP;, extended with an auxiliary …continue reading
Marijn Rol: Verification of ASD multi-component systems in mCRL2
Analytical Software Design (ASD) assists the creation of software systems. Systems designed in ASD are composed of multiple components in order to divide the complexity of the whole system over them. The verification of system properties and requirements is limited to the scope of single components, disallowing the verification of end-to-end properties. We present an …continue reading
Ziad Ben Snaiba: Logics and Algorithms for Product and Family-Based Analysis of Software Product Lines
Most model checking techniques consider single systems. With the rise of using Software Product Line Engineering (SPLE) for critical systems there is a need for model checking techniques applicable to Software Product Lines (SPL). Inspired by Classen et al. we try to devise logics to formally describe properties suitable for the analysis of SPLs. We …continue reading
Ruud van Vijfeijken: Performance evaluation of network on chip using formal models
Because of the increase in complexity of System-on-Chip (SoC) networks by using Network-on-Chip (NoC), latency has become a major issue in the design and validation. There are formal and mathematical methods to determine latency bounds of a NoC, such as network calculus, and low level simulation environments, such as a cycle-accurate simulation of the Register …continue reading