Event Category: MSc Defence

–

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

–

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

–

Variability parity games are a recently proposed extension to well-known parity games that allow for verification of software product lines (SPLs). We propose new algorithms for solving variability parity games based on the existing priority promotion and SCC decomposition, and provide new heuristics for VPGs. We implemented these proposed algorithms, as well as an algorithm …continue reading

–

OIL, short for Open Interaction Language, is a domain-specific language developed by Canon Production Printing B.V. It is a language that can be used for specifying, analyzing, and implementing models of system behavior. The tooling created for OIL can generate C++ code from OIL specifications. Part of this generated code is a scheduler that schedules …continue reading

–

Two optimizations for Zielonka’s recursive algorithm for solving parity games are investigated. The first optimization is partial re-decomposition, in which only the part of the graph containing vertices of SCCs which have 1 or more vertices removed will be re-decomposed. The second optimization is dynamic SCC maintenance, which builds an SCC tree for each SCC …continue reading

–

At Vitens, the biggest drinking water company from the Netherlands, most processes in extracting, purifying and delivering drinking water are automated using PLCs. In order to check PLC programs, translation schemes for the programming languages Function Block Diagram and Structured Text are defined into an SMT solver. Using the SMT solver, a set of typical …continue reading

–

Tarjan’s algorithm for strongly connected components is used in the mCRL2 toolset. This algorithm finds all strongly connected components or SCC in a directed graph. Here an SCC is a maximal set of nodes such that there exists a directed path between all nodes in the set. The normal implementation of Tarjan’s algorithm uses recursion. …continue reading