Scientific publications

In this paper, we introduce MIOA, a stochastic process algebra-like specification language with finite-domain datatypes, as well as the logic intSPDL, and its model checking algorithms. MIOA which stands for Markovian input/output automata language is an extension of Lynch’s input/output automata with Markovian timed transitions.

In this paper we will describe the SoftArc approach. With the SoftArc approach it is possible to model and analyse safety-critical embedded and distributed systems that consist of both hard- and software. We are going to present the SoftArc modelling language, its syntax and semantics. The semantics of the SoftArc modelling language is defined in terms of stochastic reactive modules.

When designing, adapting or extending a complex cyber physical system, it extremely difficult to guarantee that all parts cooperate correctly, especially when many parties are involved in the development process. We propose a new approach to identify and to solve problems in the early development phases, thus reducing costs in the system implementation, test and integration phases.

For preemptive scheduling, the discrete scheduling has the same capability as the continuous scheduling. However, most work previously done has been focused on the continuous scheduling. In this paper, a discrete analysis approach EmptySlots method is discussed and applied to fixed priority scheduling for constraint-deadline task model.

This paper describes efficient procedures for model checking Markov reward models, that allow us to evaluate, among others, the performability of computercommunication systems.We present the logic CSRL (Continuous Stochastic Reward Logic) to specify performability measures. It provides flexibility in measure specification and paves the way for the numerical evaluation of a wide variety of performability measures.

Nowadays, mobile devices are used more and more, and their battery lifetime is a key concern. In this paper, we concentrate on a method called battery scheduling with the aim to optimize the battery lifetime of mobile devices. This technique has already been largely theoretically studied in other papers.

This thesis considers extensions of the standard independent hidden Markov model approach previously used by TNO for modelling printer nozzles. These extensions introduce parametrised transition probabilities and incorporate interactions between neighbouring nozzles to better capture the real-world printing process.

Designing the next-generation complex distributed cyber-physical systems (dCPS) poses significant challenges for manufacturing companies, necessitating efficient design space exploration (DSE) techniques to evaluate potential design decisions and their impact on nonfunctional aspects of the systems, such as performance, reliability and energy consumption.