Scientific publications

There is a constant increase of the market expectations on the capabilities of industrial high-tech systems. To meet these expectations, designers of such systems have to explore complex solutions that ensure both functionality and maximum up-time. We describe a methodology that supports the designers in this task.

There are many classes of Petri nets for describing communicating systems. Some of these guarantee important properties, such as termination in the case of portnets. There are also many methods and tools available for their analysis and synthesis. However, when developing new methods, or benchmarking against existing ones, it is often helpful to quickly generate large sets of random models satisfying certain properties and user-defined rules.

Maintaining large, multi-language code bases is challenging because of their size and complexity. Hence, tool support is desirable. Unfortunately, off-the-shelf tools fall short by aiming for genericity instead of exploiting characteristics of the specific code bases and maintenance tasks. Our objective is to support software maintenance by facilitating the development of custom tools for static code analysis.

Many real-world problems such as internet routing are actually graph problems. To develop efficient solutions to such problems, more and more parallel graph algorithms are proposed. This paper discusses the mechanized verification of a commonly used parallel graph algorithm, namely the Bellman–Ford algorithm, which provides an inherently parallel solution to the Single-Source Shortest Path problem.

At Philips IGT, we develop and produce interventional X-ray systems. For a controller in these systems, we have an approximately five years old domain specific language. Like general programming languages, domains specific languages also evolve. These languages co-evolve together with their domain. The language used at IGT was initially created for one system instance.

The rapid advancement of communication technology realized the dream of interconnected systems. In addition to enabling scalability and flexibility of solutions, this paradigm created new system design challenges. One such challenge is to holistically address security and privacy concerns of solutions early in design while respecting the system of systems context.

Gobra is an increasingly-popular systems programming language targeting, especially, concurrent and distributed systems. Go differentiates itself from other imperative languages by offering structural subtyping and lightweight concurrency through go routines with message-passing communication. This combination of features poses interestingchallenges for static verification, most prominently the combination of amutable heap and advanced concurrency primitives.

To increase energy efficiency of receiver-dominated nodes in IoT networks, we introduce Receiver-Sensitivity Control (RSC). RSC enables a trade-off between communication range and reception efforts. This trade-off is achieved through multiple receiver-sensitivity levels that can be adjusted at run time.