Scientific publications

Many companies struggle with large amounts of legacy software that is difficult to maintain and to extend. Refactoring legacy code typically requires large efforts and introduces serious risks because often crucial business assets are hidden in legacy components. We investigate the support of formal techniques for the rejuvenation of legacy embedded software, concentrating on control components.

Two Domain Specific Languages (DSLs) have been developed to improve the development of a power control component of interventional X-ray systems of Philips. Configuration files and test cases are generated from instances of these DSLs. To increase the confidence in these instances and the generators, formal models have been generated to analyse DSL instances and to crosscheck the results of the generators.

Today’s manufacturing systems are typically complex cyber-physical systems where the physical and control aspects interact with the scheduling decisions. Optimizing such facilities requires ordering jobs and configuring the manufacturing system for each job. This optimization problem can be described as a Multi-Objective Generalized TSP where conflicting objectives lead to a trade-off space.

Synchronous dataflow graphs (SDFGs) are widely used to represent digital signal processing algorithms and streaming media applications. This paper presents several methods for binding and scheduling SDFGs on a multiprocessor platform. Exploring the state space generated by a self-timed execution (STE) of an SDFG, we present an exact method for static rate-optimal scheduling of SDFGs via implicit retiming and unfolding.

Domain Specific Languages (DSLs) provide a lightweight approach to incorporate formal techniques into the industrial workflow. From DSL instances, formal models and other artefacts can be generated, such as simulation models and code. Having a single source for all artefacts improves maintenance and offers a high return on investment of the initial modelling effort.

We evaluate the effect of applying the commercial formal technique Analytical Software Design (ASD) to an industrial project. In ASD, interfaces and software designs are modelled using a formal tabular notation. The ASD tool set supports formal checks of these models, such as deadlock freedom and interface compliance.

Exploration of design alternatives and estimation of their key performance metrics such as latency and energy consumption is essential for making the proper design decisions in the early phases of system development. Often, high-level models of the dynamic behavior of the system are used for the analysis of design alternatives.

Wireless Sensor Networks (WSNs) are commonly deployed in dynamic environments where events, such as moving sensor nodes and changing external interference, impact the performance, or Quality-of-Service (QoS), of the network. QoS is expressed by the values of multiple, possibly conflicting, network quality metrics, such as network lifetime and maximum latency of communicating a packet to the sink.

This paper proposes a modeling approach to capture the mapping of an application on a platform. The approach is based on Scenario-Aware Dataflow (SADF) models. In contrast to the related work, we express the complete design-space in a single formal SADF model. This allows us to have a compact and explorable state-space linked with an executable model capable of symbolically analyzing different mappings for their timing behavior.

Constructing a model of a system for model-based testing, simulation, or model checking can be cumbersome for existing, third party, or legacy components. Active automata learning, a form of black-box reverse engineering, and in particular Angluin’s L⋆ algorithm, support the automatic inference of a model from a System Under Learning (SUL), through observations and tests.