Events at MetaForum MF 6.131

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

The Unified Modeling Language (UML), proposed by the Object Management Group (OMG), is a general purpose modeling language which became the standard for modeling system’ structure and behaviour. A UML model offers different views of the system in the form of various diagrams. The talk’s focus are UML State Machine Diagrams, widely used to specify …continue reading

In an ongoing project on the complete axiomatization of branching probabilistic bisimulation, we are currently focusing on a cancellation property. We see a route of proving the property by means of topological arguments which seems a bit far-fetched. As a possible alternative approach we propose the notion of a stable process. A process is stable …continue reading

OIL is a domain-specific language under development at OcĂ© for specifying, analysing, and implementing software components. OIL is to have IDE support, transformations to formal modelling languages for requirement verification, and code generation towards general-purpose languages such as C++. Model-based testing is an approach to test whether the behaviour of an implementation conforms to the …continue reading

SPL verification can be costly when all the software products of an SPL are verified independently. It is well known that parity games can be used to verify software products. We propose a generalization of parity games, named variability parity games (VPGs), that encode multiple parity games in a single game graph decorated with edge …continue reading

Formal system verification is a mathematical technique for establishing whether a process meets certain design requirements. Typically, such techniques require notation in academic languages which are difficult for engineers to write and interpret. We aim to develop a new DSL for formalizing requirements that dramatically lowers the barrier of entry by introducing notation and concepts …continue reading