Rance Cleaveland: QUERY-CHECKING FOR FINITE LINEAR-TIME TEMPORAL LOGIC
This talk addresses the following problem: given a finite set of observations of system behavior, each observation itself being a finite sequence of system states, and a query consisting of a Finite LTL formula with missing subformulas, compute missing the missing subformulas that make the LTL formula true for all observations. This so-called query-checking problem …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
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 equation systems. Solving parameterised boolean equation systems with real-valued parameters is not possible in most cases. We will show that …continue reading
Roxana Paval: Modeling and Verifying Concurrent Data Structures
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
Perry van Wesel: Formal analysis of ring networks
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