Scientific publications

We describe an approach to support UML-based development of embedded systems by formal techniques. A subset of UML is extended with timing annotations and given a formal semantics. UML models are translated, via XMI, to the input format of formal tools, to allow timed and non-timed model checking and interactive theorem proving.

The way in which a system's software archive is partitioned influences the evolvability of that system. The partition of a software archive, e.g. subsystem decomposition, is mostly assessed by looking at the static (include, call) relations between the parts. In the literature history information is also taken into account to assess the partition.

Nowadays, designers resort to abstraction techniques to conquer the complexity of industrial embedded systems during the design process. However, due to the large semantic gap between the abstractions and the implementation, the designers often fails to apply the abstraction techniques. In this paper, an EIS-based (executable interface specification) approach is proposed for the embedded system design.

In this paper, we present a dynamic analysis approach to increase the understandability of a large softwareintensive system, more particularly to enable the identification of dependencies between its execution entities. This approach analyzes the execution of a software system in a top-down fashion to cope with complexity and uses execution entities such as scenarios, components, and processes rather than code artifacts such as modules, classes, or objects.

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.