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 …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 …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 …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 …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 …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 …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 …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 …continue reading
Maurice Laveaux: Abstracting real-valued parameters in parameterised Boolean equation systems
The mCRL2 tool-set utilizes parameterised boolean equation systems to verify formulas from modal mu-calculus on models written in the minimal common representation language (mCRL2). For models of real-timed systems this introduces real-valued parameters in these …continue reading