Willem Rietdijk: Compositional verification of control software UML models
Abstract: Low Code Development Platforms, such as the Cordis SUITE, facilitate formal verification in software development for industrial automation. An automated translation from Cordis models to mCRL2 enables the for- mal verification of real-world industry models. However, this approach is not without challenges. The monolithic nature of the translation can lead to state space explosions …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
Julien Schmaltz: On the definition of block and idle for xMAS automata.
xMAS is a language initially proposed by Intel for architectural modelling and verification. The main feature of xMAS is to enable a boolean encoding of liveness that can be efficiently checked using SAT-based techniques. xMAS is restricted to a small set of well-defined primitives. Recently, Verbeek et al. extended this approach to state machines. In …continue reading