- 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.
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  and LIGERO . 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.