|
|
Our research aims at the development a formal methodology for the design and analysis of heterogeneous embedded systems. Thereby, we focus on the following two areas.
For the modelling of systems, we develop the description language Quartz, which started as a variant of the synchronous programming language Esterel. It is mainly based on the concept of perfect synchrony, which lends itself well to describe concurrent reactive systems. Their programming paradigm destinguishes between micro and macro steps of the execution. While micro steps do not require time at all (at least in the programming model), macro steps do all take the same amount of logical time. As a result, concurrent threads run in lockstep, and therefore implement deterministic systems. Furthermore, this model allows to synthsise very efficient programs, especially for parallel platforms as provided by FPGAs and modern multi-core processors.
A very challenging problem for the design of complex heterogeneous embedded systems is the integration of modules written in different languages. This is often the case, since IP is spread over many suppliers, and many tasks While the usage of different languages is not a problem per se, different models of computation make a straightforward integration impossible. Therefore, we study the semantic relationships between different MoC in order to derive provable properties of the composed system or even property-preserving model transformations over MoC boundaries.
Within this context, we are also interested in models for hybrid systems, which are of importance escpecially for the modelling of physical constraints of embedded systems. Hybrid descriptions exhibit both discrete and continuous dynamic behaviour and state-of-the art techniques usually describe them by a combination of a transition systems and differential equations.
In addition to adequate modelling techniques and efficient synthesis, we aim at integrated verification and analysis procedured. Our description language Quartz was embedded into the theorem prover HOL. Based on this embedding, we are able to reason about the language itself, about the correctness of particular programs, and moreover, about the correctness of transformations and translations of programs in general. Averest does not only translate Quartz programs to labeled transition systems, which are the input of state-of-the-art model checkers, but also the sophisticated temporal logic specifications to simple fixpoint problems. For this reason, we can support a broader class of temporal specifications as e.g., past time temporal operators.
If verification tools are not able to verify a given specification, they can provided the user with a trace that violates the specification. Nevertheless, it is often still hard to find the erroneous module. To this end, we employ methods that have been originally developed for the computation of winning strategies of finite state games or the supervisory control applications (controler synthesis).
We are applying our own methods to real-world applications. As such an application, we developed a reactive system for polygon processing that can be used in various domains like motion planning in robotics. It reacts under real-time constraints and behaves provable correct in all cases, which has been proved with the help of the HOL theorem prover.
Most of our research work was implemented within our Averest system. This systems consists of several tools that support the design and verification of heterogeneous embedded systems. The compiler translates programs written in our programming language Quartz to a general-purpose intermediate format based on guarded actions. Subsequently, code in various formats can be generated. Besides code for hardware (gate netlists, HDL code) and software (C-code) synthesis, there are also possibilities to interface with model checkers like NuSMV or CadenceSMV, or with theorem povers like HOL.
Averest does not only translate Quartz programs to labeled transition systems, which are the input of state-of-the-art model checkers, but also the sophisticated temporal logic specifications to simple fixpoint problems. For this reason, we can support a broader class of temporal specifications as e.g., past time temporal operators.
|
Verification of Reactive SystemsFor a presentation of state-of-the-art verification algorithms that are implemented in Averest, see also the book Verification of Reactive Systems, which was published in the EATCS Series of Springer-Verlag. |
The following pages sketches your previous research topics as well as some projects, on which our predecessor, the VLSI Design and Architecture Group, worked until 2003.
|