Search

To aid in making software bug-free, several high-tech companies are moving from coding to modelling. In some cases model checking techniques are explored or have already been adopted to get more value from these models. This also holds for Canon Production Printing, where the language OIL was developed for modelling control-software components. In this paper, we present OIL and give its semantics. We define a translation from OIL to mCRL2 to enable the use of model checking techniques. Moreover, we discuss validity requirements on OIL component specifications and show how these can be formalised and verified using model checking. To test the feasibility of these techniques, we apply them to two models of systems used in production.

Partial-order reduction (POR) is a well-established technique to combat the problem of state-space explosion. We propose POR techniques that are sound for parity games, a well-established formalism for solving a variety of decision problems. As a consequence, we obtain the first POR method that is sound for model checking for the full modal $$\mu $$-calculus. Our technique is applied to, and implemented for the fixed point logic called parameterised Boolean equation systems, which provides a high-level representation of parity games. Experiments indicate that substantial reductions can be achieved.

Reasoning about the correctness of parallel and distributed systems requires automated tools. By now, the mCRL2 toolset and language have been developed over a course of more than fifteen years. In this paper, we report on the progress and advancements over the past six years. Firstly, the mCRL2 language has been extended to support the modelling of probabilistic behaviour. Furthermore, the usability has been improved with the addition of refinement checking, counterexample generation and a user-friendly GUI. Finally, several performance improvements have been made in the treatment of behavioural equivalences. Besides the changes to the toolset itself, we cover recent applications of mCRL2 in software product line engineering and the use of domain specific languages (DSLs).

Model checking is an effective way to design correct software. Making behavioural models of software, formulating correctness properties using modal formulas, and verifying these using finite state analysis techniques, is a very efficient way to obtain the required insight in the software. We illustrate this on four common but tricky examples.

Software has become an essential component in signalling systems. Writing clear, precise and accurate specifications is of course important for these systems. Can formal methods help in this process? An interesting case is the recent development of the Hybrid Level 3 for ERTMS/ETCS. This paper addresses the specification and demonstration of ERTMS Hybrid Level 3.

In model checking, partial-order reduction (POR) is an effective technique to reduce the size of the state space. Stubborn sets are an established variant of POR and have seen many applications over the past 31 years. One of the early works on stubborn sets shows that a combination of several conditions on the reduction is sufficient to preserve stutter-trace equivalence, making stubborn sets suitable for model checking of linear-time properties. In this paper, we identify a flaw in the reasoning and show with a counter-example that stutter-trace equivalence is not necessarily preserved. We propose a solution together with an updated correctness proof. Furthermore, we analyse in which formalisms this problem may occur. The impact on practical implementations is limited, since they all compute a correct approximation of the theory.

Parameterised Boolean Equation Systems (PBESs) can be used to represent many different kinds of decision problems. Most notably, model checking and equivalence problems can be encoded in a PBES. Traditional instantiation techniques cannot deal with PBESs with an infinite data domain. We propose an approach that can solve PBESs with infinite data by computing the bisimulation quotient of the underlying graph structure. Furthermore, we show how this technique can be improved by repeatedly searching for finite proofs. Unlike existing approaches, our technique is not restricted to subfragments of PBESs. Experimental results show that our ideas work well in practice and support a wider range of models and properties than state-of-the-art techniques.

Model checking is a technique for automatically assessing the quality of software and hardware systems and designs. Given a formalisation of both the system behaviour and the requirements the system should meet, a model checker returns either a yes or a no. In case the answer is not as expected, it is desirable to provide feedback to the user as to why this is the case. Providing such feedback, however, is not straightforward if the requirement is expressed in a highly expressive logic such as the modal µ-calculus, and when the decision problem is solved using intermediate formalisms. In this paper, we show how to extract witnesses and counterexamples from parameterised Boolean equation systems encoding the model checking problem for the first-order modal µ-calculus. We have implemented our technique in the modelling and analysis toolset mCRL2 and showcase our approach on a few illustrative examples.

We address the concept of abstraction in the setting of probabilistic reactive systems, and study its formal underpinnings for the strictly alternating model of Hansson. In particular, we define the notion of branching bisimilarity and study its properties by studying two other equivalence relations, viz. coloured trace equivalence and branching bisimilarity using maximal probabilities. We show that both alternatives coincide with branching bisimilarity. The alternative characterisations have their own merits and focus on different aspects of branching bisimilarity. Coloured trace equivalence can be understood without knowledge of probability theory and is independent of the notion of a scheduler. Branching bisimilarity, rephrased in terms of maximal probabilities gives rise to an algorithm of polynomial complexity for deciding the equivalence. Together they give a better understanding of branching bisimilarity. Furthermore, we show that the notions of branching bisimilarity in the alternating model of Hansson and in the nonalternating model of Segala differ: branching bisimilarity in the latter setting turns out to discriminate between systems that are intuitively branching bisimilar.

Linear type systems need to keep track of how programs use their resources. The standard approach is to use context splits specifying how resources are (disjointly) split across subterms. In this approach, context splits redundantly echo information which is already present within subterms. An alternative approach is to use leftover typing [2, 23], where in addition to the usual (input) usage context, typing judgments have also an output usage context: the leftovers. In this approach, the leftovers of one typing derivation are fed as input to the next, threading through linear resources while avoiding context splits. We use leftover typing to define a type system for a resource-aware π -calculus [26, 27], a process algebra used to model concurrent systems. Our type system is parametrised over a set of usage algebras [20, 34] that are general enough to encompass shared types (free to reuse and discard), graded types (use exactly n number of times) and linear types (use exactly once). Linear types are important in the π -calculus: they ensure privacy and safety of communication and avoid race conditions, while graded and shared types allow for more flexible programming. We provide a framing theorem for our type system, generalise the weakening and strengthening theorems to include linear types, and prove subject reduction. Our formalisation is fully mechanised in about 1850 lines of Agda [37].

Binary session types guarantee communication safety and session fidelity, butalonethey cannot rule out deadlocks arising from the interleaving of different sessions. In Classical Processes (CP)[53]—a process calculus based on classical linear logic—deadlock freedom is guaranteed by combining channel creation and parallel composition under the same logical cut rule. Similarly, in Good Variation (GV)[39,54]—a linear concurrent lambda-calculus—deadlock freedom is guaranteed by combining channel creation and thread spawning under the same operation, called fork. In both CP and GV, deadlock freedom is achieved at the expense of expressivity, as the only processes allowed are tree-structured. Dardha and Gay[19] define Priority CP (PCP), which allows cyclic-structured processes and restores deadlock freedom by usingpriorities, in line with Kobayashi and Padovani[34,44]. Following PCP, we present Priority GV (PGV), avariant of GV which decouples channel creation from thread spawning. Consequently, we type cyclic-structured processes and restore deadlock freedom by using priorities. We show that our type system is sound by proving subject reduction and progress. We define an encoding from PCP to PGV and prove that the encoding preserves typing and is sound and complete with respect to the operational semantics.

The project’s goal is to evaluate the author as a software designer, while providing ASML with a modern approach in designing CPD applications, which are used in an ASML machine to perform calibrations, diagnostics and performance tests. This report contains the design solution as well as a description of the process that led there. Therefore, in addition to the new design, the domain, project management conclusions, and retrospective are explained in corresponding chapters.

Part of calibration applications use specific log files, called TLG, as a way of com-munication between their different job steps. The components that provide all the necessary functionality for reading/writing data from/to TLG files are the TestLog components (family of components), thus, every client of TLG files has to communi-cate with a relevant TestLog component.TestLog has been part of the software since 2000 and at that time the Metrology domain, the software archive, and the software community were much smaller. No proper requirements had been recorded and no maintenance has been done since then. Thus the original design is not scalable enough to support multiple platforms and in order to do so new specific TestLog components were introduced.The software era from 2013 and later strives to have different release strategies and even different releases for parts of the software. With the current design, TestLog cannot follow this route; it will continue splitting. Thus the decision to start an inves-tigation for its improvement has been taken.The main issues that current TestLog is dealing are the following:• Pluggability - ability to add/remove/split/combine components without extra work and providing more/less data.• Compatibility - ability of the "new" TestLog to communicate with existing cli-entsIn order to overcome these problems a new TestLog design that gives emphasis to the software quality characteristics was created. In that way software is easier to work with, to understand and to maintain. New design brings the following changes:• Drivers register themselves automatically to TestLog.• TestLog is eliminated to one common component that is decoupled from driver data interfaces.• It stores/retrieves to/from TLG files only weak type data.• Drivers provide the needed subsets of their data through query interfaces. The latter (only the needed ones) are used by calibration applications.• TestLog communicates with drivers by using their new common interface.The benefit from the above changes is that now is possible to add/remove/combine/ split drivers or their data without putting any overhead to TestLog component (no change, no recompilation).A prototype that follows a pure object oriented approach was implemented and proved that the proposed solution is feasible and that an integration of C++ (proto-type) with C (current implementation) can be done without a significant risk.This project was the first attempt to develop a pluggable TestLog architecture and it was mostly focused on a frequently changing part of the TLG data, the machine con-stants. However the same logic can be applied to other configuration data. Last but not least, the migration strategy that was developed gives the direction of moving to the new design without introducing big risks.

ASML Lithography machines trace data are vital inputs for configuration and calibration of machine components. To visualize these trace data, ASML engineers regularly utilize Gantt chart based visualization tools. Different components of lithography machines use different data formats to log their behavior. Accordingly different departments in ASML are using different trace data visualization tools. Developing and maintaining multiple visualizer tools is costly, time consuming and reduces interoperability. This report describes a project conducted to achieve a generic and an extensible Gantt visualization tool. The tool is developed using Model Driven Engineering (MDE) methodology. To capture generic trace data attributes, Gantt figure elements and the mapping between the two languages, Gantt data, Gantt figure and Gantt mapping language are defined. Furthermore, transformation modules that transform data from one format to another are specified. The extensibility of the Gantt visualization tool is verified by porting the tool in to two different domains. The effort required to port the tool to a new domain was found to be very minimal (12 man-hours). This is a considerable gain compared to an average of four to six months that would take if the tool was developed from scratch.