Edward Liem: Extraction of Invariants in Parameterised Boolean Equation Systems
Parameterised Boolean Equation Systems (PBESs) are used to express and solve various model checking and equivalence checking problems. However, it may not always be efficient, or even possible, to find a solution to PBESs since they may encode undecidable problems. One particular technique towards finding a solution to a PBES is the concept of exploiting …continue reading
Myrthe Spronck: Fairness Assumptions in the Modal mu-Calculus
The modal μ-calculus is a highly expressive logic, but its formulae are often hard to understand. We have tools for testing if a model satisfies a model μ-calculus formula, but if we are unsure of what the formula expresses we cannot draw definite conclusions from the results. To mitigate the difficulties in designing μ-calculus formulae, …continue reading
Gijs Leemrijse: Towards relaxed memory semantics for the Autonomous Data Language
On 28 August at 10:00 in MF14, Gijs Leemrijse will defend his MSc thesis titled “Towards relaxed memory semantics for the Autonomous Data Language”. This work presents an alternative operational semantics for the Autonomous Data Language (AuDaLa) with relaxed memory consistency and incoherent memory. We show how the memory operations of our semantics can be …continue reading
Tim Beurskens: Formal Verification of Safety Properties in Automotive Systems
As the automotive industry transitions towards model-based development, the need for model-based verification arises. Although recognized institutes such as ISO and IEC recognize the benefits of formal analysis in the development of safety-critical E/E systems, specific standards or guidelines on these practices are mostly absent. There are several toolsets available for formal verification purposes. These …continue reading
Sky Sarah van Grieken: Replicating Experiments and Improving Algorithms for Exact DFA Identification
In process mining, grammatical inference is used to extract information from large amounts of data. One problem in grammatical inference is exact DFA identification: finding a smallest DFA that accepts and rejects given words. Empirical experiments are used to compare new algorithms with the state of the art for exact DFA identification. To investigate to …continue reading
Maarten Visscher: Formal verification on the Maeslant Barrier Locomobile software
The Maeslant Barrier Locomobile software controls the barrier arms of the Maeslant storm surge barrier. The actual software controller of the locomobile has been literally modelled in mCRL2. The software was described in a document of over 500 pages. Subsequently, 17 properties have been extracted from the documentation of Rijkswaterstaat, modelled as modal formulas verified …continue reading
Milan Hutten: Sound and Complete Axiomatizations for the rooted variants of Divergence-Preserving, Weak Divergence-Preserving and Stability-Respecting Branching Bisimilarity
This thesis studies divergence and the extra complexity it adds to branching bisimilarity and axiomatizations with respect to branching bisimilarity. Aceto et al. provided sound and complete axiomatization with respect to rooted branching bisimilarity over basic CCS with the prefix iteration operator. Additionally, Spaninks, and Liu and Yu proposed sound and complete axiomatizations with respect …continue reading
Kevin Jilissen: A formal analysis of the tunnel control systems of the Rijkswaterstaat GITO
On Monday, August 29, at 15:00 in MF13 Kevin Jilissen defends his master thesis called A formal analysis of the tunnel control systems of the Rijkswaterstaat GITO.
Floris Zeven: Spatial Model Checking with mCRL2
Image analysis using spatial model checking is a relatively recent approach that has promising applications in the medical field. We investigated whether it is possible to verify spatial proper- ties using the mCRL2 toolset, which was built to verify concurrent systems and protocols. This was achieved by translating Spatial Logic for Closure Spaces (SLCS) formulae …continue reading
Dennis Rizvić: Making MCA easily understandable with mCRL2
A model of multicopy semantics of low level memory operations is made in mCRL2. These memory operations can be relaxed, release, acquire and sequentially consistent, which determine whether these operations can be executed before or after surrounding instructions. Using this model it is investigated which semantics the read and write operations of Peterson’s mutual exclusion algorithm must have to work …continue reading