- Stijn Kuiper: Complete Axiomatisations of Interleaving with Deadlock and Successful Termination.
28 June 14.00 - 14.45, 2024, MetaForum MF 6.131.
Abstract: This thesis studies the ω-completeness of process theories for parallel processes without communication, extended with constants for successful and unsuccessful termination. We look into the ω-completeness of the theories BSP, which is the theory BSP extended with operators for parallel composition and left merge, as well as PA0, which is the theory PA extended with a constant 0 for deadlock. While ground-completeness results are abundant in literature, previous work has failed to address the ω-completeness of process theories that are able to make the distinction between successful and unsuccessful termination of parallel processes. We will show that the theory BSP that we introduce is ω-complete by specifying behaviour on open terms alongside a generalised notion of bisimilarity ∼ on open terms and then show that the theory BSP is sound and complete with respect to ∼, from which the ω-completeness follows. We also attempt to show the ω-completeness of PA0, but run into a significant issue, which we leave as an open problem. Finally, we present an auxiliary result on the unique decomposition of PA0 terms into a parallel composition of parallel prime components.
- Erik Pardijs: Finite bases in the linear time-branching time spectrum with sequential composition and succesful termination.
1 December 14.00 - 14.45, 2023, MetaForum MF 3.
Abstract: The process algebra TSP extends the process algebra BCCSP with sequential composition and successful termination. For BCCSP it is known, for all semantics in Van Glabbeek’s linear time-branching time spectrum of behavioural semantics, whether a finite basis exists. In this thesis, we study whether these semantics are finitely based over TSP. We discovered that none of the congruences between Ready Simulation and Completed Trace equivalence, some of which were finitely based over BCCSP, are finitely based, regardless of alphabet cardinality. We also show that 2-Nested Simulation and Possible Futures equivalence still do not have a finite, sound and ground-complete axiomatization. Furthermore, we provide a finite basis for Simulation equivalence with an infinite alphabet, Trace equivalence with a non-singleton alphabet and Language equivalence for all alphabet cardinalities.
- Jordi van Laarhoven: Formalising the State Machine Modelling Tool (SMMT).
1 December 14.00 - 14.45, 2023, MetaForum MF 13.
Abstract: Model-Driven (Software) Engineering (MDSE) is gaining popularity in industry. More and more companies acknowledge the benefits of using MDSE to develop their software components. A company that exploits model-driven software engineering is Canon Production Printing (Venlo, The Netherlands). At Canon Production Printing, the State Machine Modelling Tool (SMMT) was developed to enable the modelling of software components using state machines. In this graduation report, we present SMMT and formally define a subset of the SMMT language. A translation from SMMT specifications to mCRL2 specifications is defined to allow for model checking on the SMMT specifications. We show that this translation can correctly generate mCRL2 specifications for the existing SMMT specifications at Canon Production Printing. Furthermore, we show how the mCRL2 toolset can be used to prove the correctness of SMMT specifications.
- Jore Booy: Model-Based Mocking: Compositional Model-Based Testing for Microservices using the Axini Modeling Platform.
23 November 10.00 - 10.45, 2023, Atlas 11.201.
Abstract: Model-based testing is a compelling method for the integration testing of microservices. However, when testing with a large number of services, state space explosions are a common problem. It is especially a problem in model-based testing since the input-output conformance (ioco) relation is not compositional. We developed a novel and theoretically grounded testing method called model-based mocking (MBM) to test microservice systems by mocking the underlying services of a SUT during testing. MBM is sufficient to make component-wise testing compositional.
We tested the MBM method using the Axini Modeling platform by inserting 20 mutants into an example microservice system. In our set of inserted bugs, MBM found more than half of the bugs faster compared to other methods and was slower for none of the bugs.
- Isabelle Cooijmans: Verification of EULYNX light signal using mCRL2 and comparing with auto-translated model.
26 October 15.00 - 15.45, 2023, MetaForum MF 6.131.
Abstract:
This thesis presents the light signal case study as part of the
FormaSig project, which aims to use formal methods to support the development of EULYNX - a European initiative to standardise interfaces of signalling systems. EULYNX specifies its interfaces using SysML, which is a semi-formal modelling language. Previous research has developed a formalisation for auto-translating these SysML models to mCRL2. The first goal is to verify the SysML models of the light signal interface in mCRL2 by interpreting the SysML models directly instead of using automatic translation. The second goal is to perform a comparative study between the hand-made and the auto-translated model. The formalisation is made for all SysML models and hence has to include all SysML aspects, which can lead to enormous state space of billions of states. A case study has been executed on a smaller system - the point, which already has 5.14 · 10^10 states because of the formalisation. Hence, the auto-translated model for the light signal system might become too big for model-checking since the light signal system is larger than the point system.
The main idea behind this project is to look into the choices made for modelling and see whether these choices lead to meaningful verification of the specification and inspire improvements in the automated translation process. These improvements can then lead to improved models for the FormaSig project. An mCRL2 model is created and verified while keeping track of the choices made in the modelling process. At the end of this research, the models are checked against the specified requirements, which leads to confirming found problems in the specification. Furthermore, a comparative study between the models is executed in terms of usability, which shows a trade-off between maintainability and verifiability.
- Edward Liem: Extraction of Invariants in Parameterised Boolean Equation Systems.
28 September 09.30 - 10.30, 2023, MetaForum MF 14.
Abstract: Parameterised Boolean Equation Systems (PBESs) are used to express and solve various model checking and equivalence checking problems. However, it may not always be efficient, or even possible, to find a solution to PBESs since they may encode undecidable problems. One particular technique towards finding a solution to a PBES is the concept of exploiting global PBES invariants. Although invariants have been studied extensively, there is a lack of research towards invariant discovery and exploitation in PBESs. Our paper presents PBES invariant extraction techniques inspired from various concepts found in program verification literature well as provide new conditions for invariance properties. We also present a novel graph structure, namely relevancy graphs, which characterize relevant predicate variable instances of instantiated PBES equations. Using relevancy graphs, we illustrate how invariants interact with PBESs as well as provide an alternative criteria to proving the PBES global invariant condition in simple functions.
- Myrthe Spronck: Fairness Assumptions in the Modal mu-Calculus.
7 September 14.00 - 15.00, 2023, MetaForum MF 14.
Abstract: The modal μ-calculus is a highly expressive logic, but its formulae are often hard to understand. We have tools for testing if a model satisfies a model μ-calculus formula, but if we are unsure of what the formula expresses we cannot draw definite conclusions from the results. To mitigate the difficulties in designing μ-calculus formulae, property specification patterns have been designed to help researchers express common properties in the μ-calculus. However, existing translations of these patterns to the modal μ-calculus only allow for the inclusion fairness assumptions to a very limited degree, even though fairness assumptions are very useful when model checking. Fairness assumptions allow the researcher to specify that certain types of property violations that may exist in the model are unrealistic and should not be considered when determining if the property is satisfied. This is often required because most of the time, when researchers model systems they abstract away from certain details such as the way scheduling is done, which then results in scenarios being represented in the model that would never occur in reality. There exists, therefore, a need for a standard and proven way of including a variety of fairness assumptions in modal μ-calculus formulae for properties. We extend the existing translations from the property specification patterns to the modal μ-calculus with ways to incorporate three common fairness assumptions: weak fairness, strong fairness and fair reachability (also known as ∞-fairness or hyperfairness) of the actions in a model. We also discuss other fairness assumptions to a lesser extend, including unconditional fairness of actions and weak fairness, strong fairness and fair reachability of parts of a model other than actions. When it comes to the patterns, we start with a detailed discussion on the global response pattern, which is one of the most commonly occurring ones. We then generalise our approach to cover other patterns as well. Correctness proofs are included for both the global response formulae and the generalised formulae. We conclude we a brief discussion of how the formulae we have presented in this thesis can be used in the model checking toolset mCRL2.
- Gijs Leemrijse: Towards relaxed memory semantics for the Autonomous Data Language.
28 August 10.00 - 10.30, 2023, MetaForum MF 14.
Abstract: On 28 August at 10:00 in MF14, Gijs Leemrijse will defend his MSc thesis titled "Towards relaxed memory semantics for the Autonomous Data Language".
This work presents an alternative operational semantics for the Autonomous Data Language (AuDaLa) with relaxed memory consistency and incoherent memory. We show how the memory operations of our semantics can be safely mapped onto the NVIDIA PTX virtual ISA and demonstrate that our semantics performs faster than the original when executing AuDaLa programs on GPUs. We translate our operational semantics into an axiomatic memory consistency model and formally check, for a bounded program size, its correspondence with PTX’s memory consistency model using the Alloy model finder. We conclude by presenting AuDaLaC, our compiler targeting the CUDA platform, with which we explore several different strategies to compile AuDaLa programs. We demonstrate in several case studies that AuDaLa implementations can perform faster than sequential implementations.
- Tim Beurskens: Formal Verification of Safety Properties in Automotive Systems.
7 July 13.00 - 13.30, 2023, .
Abstract:
As the automotive industry transitions towards model-based development, the need for model-based verification arises. Although recognized institutes such as ISO and IEC recognize the benefits of formal analysis in the development of safety-critical E/E systems, specific standards or guidelines on these practices are mostly absent. There are several toolsets available for formal verification purposes. These toolsets often use a niche modeling syntax which could hinder industry adaptation. By bridging the gap between widely used modeling software such as Simulink and verification tools we could enable the adoption of formal methods in the automotive or other safety-critical industries.
This work explored how formal verification can be applied to hierarchical Simulink and Simulink Stateflow models. By dividing the models into separate subsystems we can construct large hierarchical models in mCRL2 syntax, similar to the original hierarchy in Simulink. Several blocks in the Simulink block library have been translated to a functionally similar variant in mCRL2. Instances of these implementations can be placed in dataflow diagrams to obtain complex behaviour from a collection of simple processes. This process has been partially automated using a code generator which interprets mCRL2 design files as templates. This can reduce code repetition and makes the design process easier.
The approach has been demonstrated on a small toy example of the Collatz sequence, as well as a model from Mathworks’ examples repository, modeling a traffic intersection with two traffic lights. It could be demonstrated that the two variants of the Collatz model both converged to 1 for any of the given initial conditions.
The traffic light example model featured both dataflow blocks, virtual (subsystem) blocks and hierarchical Stateflow charts in which message queues are used to communicate between charts. Most effort in translating this model went into the Stateflow controller model, as this model used several Stateflow features (message queues and hierarchical charts) with limited documentation. As there is no formal definition of a dataflow or Stateflow diagram, the translation to mCRL2 has no formal basis. It can therefore not be demonstrated that the translation results in functionally equivalent models compared to the Simulink sources.
A SMT-based scheduling tool has been used to overcome the issue of incorrect schedules in dataflow diagrams due to an incorrect port ordering. This tool computes a satisfying schedule based on a simplified representation of the dataflow diagram. The resulting schedule can be imported in the template preprocessor to re-order the output ports.
- Sky Sarah van Grieken: Replicating Experiments and Improving Algorithms for Exact DFA Identification.
25 May 10.30 - 11.30, 2023, MetaForum MF 6.131.
Abstract: In process mining, grammatical inference is used to extract information from large amounts of data. One problem in grammatical inference is exact DFA identification: finding a smallest DFA that accepts and rejects given words. Empirical experiments are used to compare new algorithms with the state of the art for exact DFA identification. To investigate to what extend the research field of formal verification is affected by the replication crisis, we replicate the existing experiments to see if their results are valid. We also run new experiments for exact DFA identification to test if the assumptions in existing papers are valid and to test if the performance of SAT and SMT solvers with new combinations of existing algorithms and symmetry breaking predicates can be improved. This thesis provides a program with all the state-of-the-art algorithms and symmetry breaking predicates of exact DFA identification, with which our experiments are easy to reproduce. With these experiments, we show that the replication crisis also affects the field of formal verification and replicating experiments can be made more attractive by also investigating new research questions with the replicated code.
- Maarten Visscher: Formal verification on the Maeslant Barrier Locomobile software.
15 May 15.00 - 15.45, 2023, MetaForum MF 14.
Abstract: The Maeslant Barrier Locomobile software controls the barrier arms of the Maeslant storm surge barrier. The actual software controller of the locomobile has been literally modelled in mCRL2. The software was described in a document of over 500 pages. Subsequently, 17 properties have been extracted from the documentation of Rijkswaterstaat, modelled as modal formulas verified on the model. The verification includes the full behaviour, including well defined erroneous behaviour, for instance due to faulty sensors, except for a limited number of situations that caused the statespace to grow too much.
This project clearly shows that it is possible to verify actual control software that occur storm barriers.
- Milan Hutten: Sound and Complete Axiomatizations for the rooted variants of Divergence-Preserving, Weak Divergence-Preserving and Stability-Respecting Branching Bisimilarity.
21 December 13.00 - 14.15, 2022, MetaForum MF 6.131.
Abstract: This thesis studies divergence and the extra complexity it adds to branching bisimilarity and axiomatizations with respect to branching bisimilarity. Aceto et al. provided sound and complete axiomatization with respect to rooted branching bisimilarity over basic CCS with the prefix iteration operator. Additionally, Spaninks, and Liu and Yu proposed sound and complete axiomatizations with respect to rooted divergence-preserving branching bisimilarity over basic CCS with the recursion construct. We contribute by providing a sound and complete axiomatization with respect to rooted divergence-preserving branching bisimilarity over basic CCS with the prefix iteration operator. Additionally, we provide sound and complete axiomatizations with respect to rooted weakly divergence-preserving branching bisimilarity and rooted stability-respecting branching bisimilarity over the same algebra and show that completeness of these axiomatizations and the axiomatization with respect to rooted branching bisimilarity provided by Aceto et al. can be derived from the completeness of the axiomatization with respect to rooted divergence-preserving branching bisimilarity. Lastly, we discuss how the prefix iteration operator can be expressed through the recursion construct and partially show how our proposed axiomatization is represented in the axiomatizations of Spaninks, and Liu and Yu.
- Kevin Jilissen: A formal analysis of the tunnel control systems of the Rijkswaterstaat GITO.
22 August 15.00 - 15.45, 2022, MetaForum MF 13.
Abstract: On Monday, August 29, at 15:00 in MF13 Kevin Jilissen defends his master thesis called A formal analysis of the tunnel control systems of the Rijkswaterstaat GITO.
- Floris Zeven: Spatial Model Checking with mCRL2.
23 June 15.00 - 15.45, 2022, MetaForum MF 6.131.
Abstract: 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 to μ-calculus formulae, proving this translation is correct, and by creating a script that associates an mCRL2 specification with an image. As mCRL2 only verifies properties on an initial state, which would correspond to a single pixel, a proof-of-concept implementation was subsequently created that utilizes the mCRL2 toolset to mark every pixel that satisfies a spatial property.
- Dennis Rizvić: Making MCA easily understandable with mCRL2.
29 April 15.00 - 15.45, 2022, MetaForum MF 12.
Abstract: 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 correctly.
- Koen Degeling: New algorithms and heuristics for solving Variability Parity Games.
19 November 14.00 - 14.45, 2021, MetaForum MF 2.
Abstract: 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 based on Jurdzinski’s small progress measures. We compare existing algorithms for solving VPGs and the impact of different pre-processing steps and propose a method to generate random variability parity games.
- Tom Buskens: Optimizing the code generator for OIL.
6 October 10.30 - 11.15, 2021, Atlas 1.652.
Abstract: 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 so-called proactive events. The focus of this project is to improve this scheduler; the aim is to reduce the number of computations needed to do the scheduling. We investigate basic scheduling improvement strategies that do not need the collection of additional information. We also investigate scheduling strategies for which causal relations have to be gathered from the OIL specifications. These scheduling strategies could be used to skip the scheduling of events that are not needed. Another strategy that we investigate alters the OIL specifications themselves to make them easier to schedule. In this report, these strategies for improving the scheduler are discussed, verified, and achieved results are listed.
- Anneke Huijsmans: Optimising parity game solvers using dynamic SCC maintenance.
13 September 14.00 - 14.45, 2021, MS Teams.
Abstract: 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 and then maintains those when vertices or edges are removed from the graph. An implementation in Java is made for 3 versions of Zielonka’s algorithm: the first version is Zielonka’s algorithm with Tarjan’s algorithm as described in literature. The second version is Zielonka’s algorithm with the use of partial re-decomposition. The third version is Zielonka’s algorithm with dynamic SCC maintenance. The 3 versions are tested on various games. The conclusion from the tests is that Zielonka’s algorithm with partial re-decomposition gives the best improvement.
- Jasper Stam: Formal verification of an industrial PLC program in Function Block Diagram and Structured Text.
16 August 14.15 - 15.00, 2021, Atlas 8.340.
Abstract: 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 properties could be checked on a PLC program with the size typical for PLC programs within Vitens. Most properties could be shown to hold (and all could be (dis)proven in matters of seconds), although virtually all initially formulated properties required fine tuning before they could be shown valid.
The overall conclusion is that the use of SMT solvers is very effective in analysing industrial scale PLC software.
- Geert van Ieperen: Visualisation of large Labelled Transition Systems.
22 April 15.00 - 15.45, 2021, MS Teams.
Abstract: A formal model describes the behaviour of a program, protocol or other system. The properties of this model can be verified, such that we can prove these properties with absolute certainty. Visualising the state space of a formal model is an important tool for their development. This thesis focuses on visualising such a state space as a graph.
We present a layout technique that provides efficient graph layouts for graphs with over 10000 nodes, discuss the effectiveness of different edge shapes, and present multiple ways of highlighting the structure of the graph. We present a rendering procedure capable of rendering graphs larger than 10000 nodes while supporting these techniques. We implemented these techniques in a tool and use it to measure the performance of the techniques. The effectiveness of these techniques is analysed using a survey on the tool in a few practical applications.
We conclude that these techniques can effectively be used in one visualisation to assist in formal model development.
The tool is registered on DOI 10.5281/zenodo.4680646
- Wouter Schols: Verification of an iterative implementation of Tarjan’s algorithm for Strongly Connected Components using Dafny.
27 November 13.00 - 13.45, 2020, MS Teams.
Abstract: 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. Unfortunately, this implementation can cause stack overflow problems if the graphs are sufficiently large. The mCRL2 toolset uses an iterative implementation of Tarjan’s algorithm to circumvent this problem. In this project both the recursive and the much more complex iterative algorithm have been proven correct using the verification language Dafny. For the recursive algorithm a previous proof was already available. However this proof was nearing the limits of Dafny’s capabilities, which caused unstable results after minor changes. As part of this work techniques have been introduced to guarantee much more stable proofs.
- Bram Hooimeijer: Model Inference for Legacy Software in Component-Based Architectures.
21 October 10.00 - 10.30, 2020, MS Teams.
Abstract: Bram Hooimeijer did do his research for the master thesis at ASML. The question was whether it is possible to construct models for the behaviour of software out of a single trace using information about the software architecture. Bram showed that it was possible to come up with a reasonable model that could even be finetuned by analysing the obtained model, for instance for deadlocks and by adding meta information to the model for instance about the allowed ordering of certain events in the software.
- Nikita Golovliov: Verification of Multiprocessor System Memory Model.
21 September 13.30 - 14.00, 2020, MS Teams.
Abstract:
In a shared memory multiprocessor system, the memory model determines the outcome of read operations at any time, given a partial order of memory operations induced by processor-issued writes and reads. A memory model may pertain to high-level language semantics or hardware program execution.
This thesis focuses on verification of hardware memory model conformance, i.e. given a hardware specification and memory model, verifying whether all the possible executions of any program on the hardware are permitted by the memory model, and vice versa.
View-based definitions of a memory model require existence of a certain order between memory modification and observation events, called view. If, and only if, there exists a view that is consistent with the memory model for every execution of any program by a multiprocessor system, then the multiprocessor system conforms to the memory model.
Given a generic high-level processor-memory interface, we provide a translation of the release consistency hardware memory model to a set of linear temporal logic properties. We analyse the correctness of the translation and the deficiencies of the approach. We discuss the relation of the hardware memory model to the memory model of C++.
We provide an example multiprocessor system design that is used for verifica- tion of memory model conformance, and the guidelines for applying the properties to a real-world system.
- Wessel Sinnema: Verifying memory consistency in mCRL2.
21 September 10.00 - 10.30, 2020, Atlas 2.215.
Abstract: We present a general method to verify an mCRL2 model of a multiprocessor with respect to memory consistency and prove the correctness of this method.
Consequently, we present a way to reformulate most memory models that are defined in terms of serial views using observations. We prove that any execution of a program by a multiprocessor satisfying this formulation is memory consistent under the original memory consistency model. We then express this as a set of predicates on the traces allowed by an mCRL2 model and prove that if all traces allowed by the mCRL2 model satisfy these predicates, then all executions allowed by the mCRL2 model are consistent with respect to the original memory consistency model.
We also formulate a subset of the C++ memory model in terms of serial views. We prove that if such that serial view exists for every execution allowed by a multiprocessor, then every execution allowed by that processor is consistent under the C++ memory model. The predicates on mCRL2 traces are then expressed as mu-calculus formulas and are used to verify an mCRL2 model of a multiprocessor with respect to local consistency and cache consistency, which are subsets of the serial view representing the C++ memory model. We use these mu-calculus formulas to benchmark the verification an example CPU model using the mCRL2 toolset.
- Sebastiaan Verhoek: SMT solver verification of ladder logic in a production environment (Tata Steel).
18 August 15.30 - 16.00, 2020, Atlas 2.320.
Abstract: It is shown how to verify requirements on the PLC code in use at Tata Steel. A translator from PLC programs to the input language for SMT solvers has been written. Subsequently, requirements on some of the largest PLC programs available at Tata steel have been written down, and their validity on the software has been validated.
- Elbert van de Put: Ant Colony Optimization for Model Checking.
19 February 14.30 - 15.15, 2020, MetaForum MF 2.
Abstract: Ant Colony Optimization is an optimization algorithm that is inspired by the foraging behavior of ants. In this thesis I have applied Ant Colony Optimization to problems that are generated from the model checking problem, to Boolean equation systems and to parity games. The results of this research are mixed but we have discovered approaches where further research seems promising.
- Mark Frenken: Code Generation and Model-Based Testing in Context of OIL.
10 December 10.00 - 10.45, 2019, MetaForum MF 6.131.
Abstract: 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 behaviour described in a formal model. A notable benefit of this approach is the automated test derivation and execution. This master thesis presents a C++ code generator for OIL, implemented in the Spoofax language workbench. The correctness of the code generator is validated by means of model-based testing, implemented in JTorX.
- Sjef van Loo: Verifying SPLs using parity games expressing variability.
6 November 13.00 - 13.45, 2019, MetaForum MF 6.131.
Abstract: 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 labels expressing variability between the parity games. We show that a VPG can be constructed from a modal μ-calculus formula and an FTS that models the behaviour of the different software products of an SPL. Solving the resulting VPG decides for which products in the SPL the formula is satisfied. We introduce several algorithms to efficiently solve VPGs and exploit commonalities between the different parity games encoded. We perform experiments on SPL models to demonstrate that the VPG algorithms indeed outperform independently verifying every product in an SPL.
- Stan Roelofs: Automatically proving equality of infinite sequences.
2 October 15.00 - 15.45, 2019, MetaForum MF 7.084.
Abstract: First order inductive theorem proving deals with proving new equations based on a given set of equations. More specifically, we are interested in proving that the axioms logically imply the goals. In this presentation I will discuss how we can automate these proofs by induction. The equations can either describe finite or infinite terms. In this talk we are mainly interested in applying these ideas of induction on infinite objects. The focus is on the most simple form of infinite objects: infinite sequences of some basic data type. Using a special operator take we can also apply our induction techniques on infinite data. Finally we describe how our techniques can be implemented in practice.
- Msc presentation Johri van Eerd.
26 August 15.00 - 15.30, 2019, Atlas 2.215.
Abstract: Johri van Eerd will present his master thesis research on Monday August 26 at 15:00 in Atlas 2.215. His presentation addresses the question on whether term rewriting on GPUs is competitive compared to term rewriting on CPUs.
- Kevin Nogarede: An approachable language for formal requirements.
12 August 14.00 - 14.45, 2019, MetaForum MF 6.131.
Abstract: 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 that are intuitively understandable yet still amenable to automated verification. The applicability of the new language is assessed via user experience reports
- Ruud Meeuws: Model Checking Supermodels Workbench with mCRL2.
26 June 14.00 - 14.30, 2019, Atlas 11.201.
Abstract: At Sioux, a model-driven development tool is created. It allows users to create a model and generate software for specific hardware platforms. For this tool, Sioux wants to incorporate model checking in order to improve the correctness and safety of software. To see whether model checking is viable for industrial models, we want to explore the possibilities in limiting behaviour such that model checking becomes feasible. We specify several execution models and see the influence of
them on the efficiency and feasibility of model checking with mCRL2 for this development tool.
- Mark Bouwman: A model-based test platform for rail signalling systems.
5 February 11.00 - 11.45, 2019, MetaForum MF 3.
Abstract: As technology progresses, newer, and more complex, solutions are employed to verify that rail signalling systems are safe. Formal methods provide ways to increase rigour in the verification process. This precision, accompanied by the ongoing increase of computational power of computers, also opens up ways to partially automate parts of the verification process. We present a case study an application of mCRL2 and the model-based testing tool JTorX in the signalling domain. The mCRL2 toolkit is used to formally model the behaviour of a system at the core of signalling solutions: the interlocking. The behaviour of the interlocking is validated through model checking, proving that relevant safety properties hold. Using JTorX, the formal model is turned into the benchmark in an automated testing platform for interlocking software. A working setup with actual interlocking software on a pre-existing testing platform is presented, though performance and stability remain an issue. The suitability of mCRL2 and JTorX in the signalling domain is evaluated and suggestions are given for improvement and further research.
- Hong Zhang: Quality metrics for ASOME data models.
15 November 14.00 - 14.45, 2018, Metaforum MF3.122.
Abstract: At ASML the ASOME data modelling language has been defined. Many system designers are defining models in this language, and the question is whether there is an easy way to assess that these models are ok. This can be done using metrics. The question is which metrics are proper. In this MSc research various metrics from different sources are collected. The suitability of these metrics to indicate the complexity and maintainability of the models is assessed by questionaires and qualitative interviews.
- Ferry Timmers: A complete axiomatisation for probabilistic trace equivalence.
7 November 14.00 - 14.45, 2018, MetaForum MF 4.
Abstract: In the thesis a sound and complete axiomatisation is given for probabilistic trace equivalence for finite probabilistic processes. The axiomatisation is remarkably complex, which may explain that nobody formulated such a complete axiomatisation yet.
- Lisette Sanchez: Learning software behavior through active automata learning with data.
14 August 16.00 - 16.45, 2018, MetaForum MF 13.
Abstract: 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 can be learned, outperforming the learning of automata with concrete data. Scale remains a problem, though.
- Lois Nijland: Adding sequential composition and termination to the linear time – branching time spectrum.
24 July 10.00 - 10.45, 2018, MetaForum MF 14.
Abstract: 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 semantics for the process theories BSP and TSP. We provide a template for proving soundness and ground-completeness for BSP and apply this template to BSP modulo trace semantics. We prove that for BSP modulo ready simulation semantics with a finite number of actions of at least one a finite basis does not exist by giving an infinite family of equations which are sound but cannot be derived from a finite collection of axioms that are sound for BSP modulo ready simulation semantics. We show that we cannot use this family of equations to prove whether TSP modulo ready simulation semantics affords a finite basis. Finally, we prove that TSP modulo bisimulation is omega-complete when there is at least one action.
- Astrid Belder: Decidability of bisimilarity and axiomatisation for sequential processes in the presence of intermediate termination.
23 July 15.00 - 15.45, 2018, MetaForum MF 14.
Abstract: 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 operator that is used to remove intermediate termination from terms. Additionally, it is shown that TSP^{;} does not afford a ground-complete axiomatisation with respect to bisimilarity without an auxiliary operator. Second, we prove that bisimilarity is decidable for processes definable by finite guarded recursive specification over TSP^{;}. This is done by showing that every guarded recursive TSP^{;}-specification can be transformed to a normal form, which allows us to eliminate redundant intermediate termination from processes. Using this normal form, the existing decidability proofs for context-free processes without intermediate termination, can be adapted for TSP^{;}.
- Marijn Rol: Verification of ASD multi-component systems in mCRL2.
2 July 10.00 - 10.45, 2018, MetaForum MF 13.
Abstract: 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 approach for the verification of end-to-end properties on multi-component systems. This provides a higher confidence in the functional correctness and reliability. A system based on a real-life ASD model serves as use-case for the proposed approach. Results show that verification of multi-component systems can be done through mCRL2, but scalability issues are observed as larger systems are verified.
- Ziad Ben Snaiba: Logics and Algorithms for Product and Family-Based Analysis of Software Product Lines.
18 May 10.00 - 10.45, 2018, Flux 1.10.
Abstract: 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 attempt to provide logics for both product-based and family-based model checking based on CTL. These logics allow both nested (nCTL) and single (sCTL) product-family restrictions on the specification of the SPL. Also, we provide an equivalence between nCTL and sCTL, and algorithms for both product-based and family-based model checking using sCTL and nCTL. A small toolset to use the algorithms in practice will be provided.
- Ruud van Vijfeijken: Performance evaluation of network on chip using formal models.
13 March 10.00 - 10.45, 2018, MetaForum MF 3.
Abstract: 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 Transfer Level. This thesis proposes a method that abstracts away from low level analysis and uses a formal model to analyze the latency bounds of a given NoC. By applying different traffic schemes we can determine worst case latency of some case studies, which include a 8-node Spidergon with cache coherency and a TornadoNoC architecture.
- Maurice Laveaux: Abstracting real-valued parameters in parameterised Boolean equation systems.
30 January 14.00 - 14.45, 2018, MetaForum MF 14.
Abstract: 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 a region abstraction, derived from a similar notion defined for timed automata, can also be applied to parameterised boolean equation systems. An alternative abstraction where regions are combined into so-called zones will be defined as well. In some cases this approach works better in practice. However, it is also more restricted in the type of model checking questions that it can answer. Finally, we will define suitable representations for regions and zones that have also been implemented using the mCRL2 language.
- Roxana Paval: Modeling and Verifying Concurrent Data Structures.
25 January 14.00 - 14.45, 2018, MetaForum MF 14.
Abstract: 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 execution that respects the runtime ordering of methods. This work proposes building two process specifications of the object using the mCRL2 language. The concrete specification is built according to the implementation of the concurrent data structure, while the abstract specification is linearizable by construction. Then, linearizability can be tested by checking that their respective labeled transition systems, generated from the mCRL2 tool, are equivalent. This approach was applied on a number of concurrent data structures, and it detected both correct and faulty implementations.
- Perry van Wesel: Formal analysis of ring networks.
23 November 14.30 - 15.30, 2017, MetaForum MF 14.
Abstract: 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 to model and verify liveness of networks. Although MaDL is a useful tool for the verification of networks, it lacks the capability to completely model and analyse ring networks. Therefore, MaDL is extended with a new primitive and a ring detection algorithm that cooperate to generate additional network invariants specifically for ring networks. These extensions are used in two case studies to model and verify network architecture proposals from literature. The analysed networks are TornadoNoC [10] and LIGERO [1]. In both case studies, the process of formally modelling these architectures reveals ambiguity in the original proposal papers. Both architectures turn out to contain deadlocks when modelling as close to their original proposal as possible. The results show formal modelling is a useful tool to eliminate ambiguity, but still requires improvement to allow it to scale to larger networks. The extensions to MaDL prove to be useful when modelling certain networks, but can still be improved to allow verification of a wider range of different networks.
- Olav Bunte: Quantitative model checking on probabilistic systems using plmu*+.
21 November 10.00 - 11.00, 2017, MetaForum MF 3.
Abstract: Although most model checking logics focus on proving qualitative properties, with the logic plmu*+ introduced in Mio's PhD thesis one can check the probability that some behaviour happens. In this work we try to bring this logic to practice. We attempt to find intuitive meaning for plmu*+-formulas with the aim to create guidelines to create meaningful formulas. Also, we give an alternative representation of a plmu*+ model checking problem in form of an equations system and we give an algorithm to extract the solution from this representation, based on the work of Mader. This algorithm will be compared to an approximation algorithm by applying both on a number of use cases.