Modelling the behaviour of a system, and stepwise refining that model until it has become sufficiently detailed to generate executable implementation is an appealing approach to software development, advocated by companies such as, e.g. Verum. The approach is rooted in solid mathematics and supported by tools, such as mCRL2, that help the developer. Under the …continue reading

Model checking approaches to software product lines are doubly cursed. Not only high-dimensionality regarding the number of states may be troublesome, also the exponential number of options for a product raises a computational hindrance. In order to mitigate the latter, family-based verification, as opposed to product-based verification, has been proposed. In this talk we consider …continue reading

In this presentation, I shall introduce Autonomous Data Language, highlight its most important attributes and explain the main concepts of the language using some examples.

The principal objective of our ongoing IRF project “Programs in the wild: Uncertainties, adaptability, and verification” is to provide a formal framework and tools for modelling and verifying the behaviour of systems characterised by a close interaction of a program with an unpredictable environment, like Cyber-Physical Systems (CPSs). In this talk we will discuss the …continue reading

Almost all practical software systems today are configurable. Huge configuration spaces, usually of size exponential in the number of configuration options or features, render their design, analysis, and explanation challenging tasks. In this talk, I will introduce the notion of “feature causality” to support explainability of configurable systems. Inspired by the seminal definition of actual …continue reading

Quite some time ago I presented an approach to represent BDDs more compactly. The approach could be used to represent some formulas exponentially more compact than in ordinary BDDs. However, it was not possible to prove that this representation was never more than polynomially larger than BDDs. This approach turned out to be a particular …continue reading

A well known technique to reduce the impact of the state space explosion problem problem is compositional minimisation. In this technique, first the state spaces of all components are computed and minimised modulo some behavioural equivalence (e.g., some form of bisimilarity). These minimised transition systems are subsequently combined to obtain the final state space. In …continue reading

Model based testing (MBT) provides an efficient and automated approach to finding discrepancies between software models and their implementation. If we want to incorporate MBT into the software development process, i.e. code changes are only accepted if the implementation remains in conformance with the model, then MBT must be able to thoroughly test the entire …continue reading

In previous presentations about OIL I have mainly dived into its semantics, but in this presentation I’ll focus on its implementation in the Spoofax language workbench instead, which has been ongoing work for 5 years now. I’ll discuss how we tackled different implementation aspects of a language, such as syntax, transformations and static semantics, and evaluate …continue reading