Event Category: MSc Defence

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

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

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

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

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

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