Anna Stramaglia: Semantics of UML State Machine Diagrams – overview and ambiguities
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
Thomas Neele: Compositional Learning of Synchronous Automata
The classical L* algorithm for learning DFAs runs in polynomial time with the size of the DFA being learnt. However, the DFA that represents a system consisting of multiple parallel components can grow exponentially in the number of components; known as the state space explosion problem. In this talk I will demonstrate how, given the …continue reading
Erik de Vink: In search of for stability: cancelativity for probabilistic bisimulation
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
Mark Bouwman: Verifying the EULYNX level crossing
Even though the behaviour of the EULYNX specification of the level crossing is conceptually quite simple, the state space associated to the mCRL2 model is enormous. This Thursday I will present the reasons for the state space explosion and the measures we took to drastically reduce it. Moreover, I will present the verification efforts, which …continue reading
Jos Baeten: Integration of automata theory and process theory
Since 2007, I have been working on a project to integrate automata theory and process theory. The motivation is to present students with a model of a computer in a basic course on the foundations of computer science, that relates more closely to computers as they know them. A recent result in this project is …continue reading
Mark Frenken: Code Generation and Model-Based Testing in Context of OIL
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
Sjef van Loo: Verifying SPLs using parity games expressing variability
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
Kevin Nogarede: An approachable language for formal requirements
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
Anton Wijs: The SLCO Framework for Verified, Model-driven Construction of Component Software
I will present the Simple Language of Communicating Objects (\SLCO) framework, which has resulted from our research on applying formal methods for correct and efficient model-driven development of multi-component software. At the core is a domain specific language called SLCO that can be used to specify software behaviour. One of the features of the framework …continue reading
Tim Willemse: Explorations of Attribute-Based Access Control
Attribute-Based Access Control (ABAC) is emerging as the de facto paradigm for the specification and enforcement of access control policies. Nonetheless, ABAC is vulnerable to attribute hiding attacks where users can obtain a more favourable decision by hiding some of their attributes. The extended evaluation of an ABAC policy takes such attribute hiding into account …continue reading