Scientific publications

Conformance testing for labeled transition systems starts with defining when an implementation conforms to its specification. One of the formal theories for model-based testing uses the implementation relation ioco for this purpose. A peculiar aspect of ioco is to consider the absence of outputs as an observable action, named quiescence.

During the last three years, we have been experimenting with the use of the Uppaal model checker in an introductory course on operating systems for first-year Computer Science students at the Radboud University Nijmegen. The course uses model checkers as a tool to explain, visualize and solve concurrency problems.

In this paper we will extend the input-to-state stability (ISS) framework to continuous-time discontinuous dynamical systems (DDS) adopting non-smooth ISS Lyapunov functions. The main motivation for investigating non-smooth ISS Lyapunov functions is the success of “multiple Lyapunov functions” in the stability analysis of hybrid systems.

The software design is one of the most challenging tasks during the design of a mechatronic system. On one hand, it has to provide solutions to deal with concurrency and timeliness issues of the system. On the other hand, it has to glue different disciplines (such as software, control and mechanical) of the system as a whole.

The complexity of designing hardware/software systems motivates research on frameworks that structure and automate the design process. Such design methodologies reduce the risk of expensive design–implementation iterations by assisting designers in constructing models. Software/Hardware Engineering (SHE) is a general-purpose system-level design methodology that supports analysing both functional correctness and performance properties.

This paper presents a new (geometrical) approach to the computation of polyhedral (robustly) positively invariant (PI) sets for general (possibly discontinuous) nonlinear discrete-time systems possibly affected by disturbances. Given a β-contractive ellipsoidal set E, the key idea is to construct a polyhedral set that lies between the ellipsoidal sets β E and E.

All aspect orientation languages provide a onesize-fits-all methodology for reflection on join points. However, the amount of resources necessary for this approach is too high to be applicable in the context of consumer products. In this industrial research paper, we describe a solution to this problem and prove via an experiment that it is suitable for our context.

Formal theories for real-time systems (such as timed process algebra, timed automata and timed petri nets) have gained great success in the modeling of concurrent timing behavior and in the analysis of real-time properties. However, due to the ineliminable timing differences between a model and its realization, synthesizing a software realization from a model in a predictable way is still a challenging research topic.