Publications

The energy efficiency of an Internet of Things (IoT) receiver can be improved by introducing an adjustable tradeoff between signal quality and energy consumption. In good channel conditions, the receiver can be set to consume less energy per bit, without compromising signal quality in bad channel conditions.

In the last couple of years several dynamically-typed, object-oriented programming languages have been equipped with optional static type checkers. This typically requires these languages to be extended with a downcast operator, which is a common operator in statically-typed languages but not in dynamically-typed languages.

A key challenge in the synthesis and subsequent analysis of supervisory controllers is the impact of state-space explosion caused by concurrency. The main bottleneck is often the memory needed to store the composition of plant and requirement automata and the resulting supervisor. Partial-order reduction (POR) is a well-established technique that alleviates this issue in the field of model checking.

Rijkswaterstaat staat voor een enorme uitdaging wat betreft vervangen en renovatie (VenR) van objecten. Momenteel behelst dit voor elk object maatwerk, wat flexibiliteit biedt, maar ook bijzonder inefficiënt is. Voor het specificeren, ontwerpen, realiseren en testen van veilige besturingssoftware voor het object werkt het programma Industriële Automatisering Sourcing (IAS) daarom aan standaardisatie.

The target of the Vraaggestuurde Programma (VP) ESI is to drive advances in high-tech systems development by embedding cutting-edge engineering methodologies in the Dutch high-tech systems industry to cope with the ever-increasing complexity of their products: (i) creating impactful and industrially applicable methodologies and (ii) providing support to the high-tech industry to apply the results.

Applying Model-Driven Engineering can improve development efficiency. But gaining such benefits for legacy software requires models, and creating them manually is both laborious and error prone. Active automata learning has the potential to make it cost-effective, but practitioners face practical challenges applying it to software components of industrial cyber-physical systems.

In runtime verification, a monitor is used to return a Boolean verdict on the behavior of a system. We present several exaniples of the use of monitors to instead document system behavior. In doing so, we demonstrate how runtime verification can be combined with techniques from data science to provide novel forms of program analysis.

The ComMA language has been developed to specify interfaces of software components, including protocol state machines, time and data constraints, and constraints on relations between events of multiple interfaces. The language has been devised in close collaboration with an industrial partner where it has been used to model a large number of interfaces.

Model-based testing involves testing a system under test for conformance to a model that specifies its behaviour. An important aspect for model-based testing is the implementation relation that defines precisely when a system under test conforms to its model. The implementation relation ioco has often been used and studied in model-based testing when models are expressed as labelled transition systems, and there are tools implementing ioco-based test generation.

Industrial Cyber-Physical Systems (CPS) are complex heterogeneous and distributed computing systems, typically integrating and interconnecting a large number of subsystems and containing a substantial number of hardware and software components. Producers of these distributed Cyber-Physical Systems (dCPS) face serious challenges with respect to designing the next generations of these machines and require proper support in making (early) design decisions to avoid expensive and time consuming oversights.