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

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

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

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

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

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

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 equation systems. Solving parameterised boolean equation systems with real-valued parameters is not possible in most cases. We will show that …continue reading

Concurrent data structures can be used to communicate between parallel processes in a system. The challenge in manipulating these objects arises from the many possible ways in which the processes can interleave. To ensure correct executions, the system should fulfill linearizability. Verifying linearizability consists of checking that every concurrent execution is equivalent to some sequential …continue reading

Systems-on-Chips rely on the correct functioning of the communication between their components. As these systems grow more complex, so do the underlying communication networks. Simulating a network does not guarantee the entire state-space is explored, therefore formal verification methods should be used to ensure correctness of these Networks-on-Chips. This thesis uses the MaDL modelling language …continue reading