direkt zum Inhalt springen

direkt zum Hauptnavigationsmenü

Sie sind hier

TU Berlin

Page Content

Project VATES2

-- Continuation Project --

supported by the German Research Foundation (DFG)

Verification and Transformation of Embedded Systems

The aim of the VATES project, funded by the German Research Foundation (DFG), is the development of methods for the construction and verification of embedded real-time systems. Beside the complexity of such systems, a particular challenge is coping with concurrency aspects and real-time requirements. A distinguishing feature of the VATES project is that we consider the whole development chain from abstract specifications through source code down to
compiler-generated executable machine code. To ensure the correctness of our proofs and to gain a high degree of automatization, the verification is carried out with machine assistance, especially model checkers, SAT/SMT-solvers, and mechanical provers (like the interactive theorem prover Isabelle/HOL).

In the first phase of the VATES project, we developed a novel approach that allows us to formally relate an abstract process-algebraic specification formulated in the timed process calculus Timed CSP with its implementation given in the LLVM compiler intermediate representation. Using this relation, we are able to verify safety, liveness, and timing properties on the level of Timed CSP and transfer them to the level of executable code.

In the second phase of VATES, we extend our methodology in two directions. First, we support the verification of multicore systems, which are more and more used in the context of embedded systems. To this end, we include directives that guide the transformation for multicore target architectures into our methodology on the specification level. These can then be exploited in subsequent verification steps. Second, our methodology is extended such that adaptive systems (which
dynamically restructure themselves in changing environments) can be specified, verified, and transformed into executable, semantically equivalent code.

As a case study, we use the real-time operating system BOSS for embedded systems, which was developed by Fraunhofer FIRST (Berlin), as in the first project phase. It is employed, for example, in satellites, medical applications and an electronic lottery system. Furthermore, it is well suited for verification purposes because of its comparatively simple structure and its relatively small size. In this phase, BOSS is extended to support multicore architectures and to directly include mechanisms that support adaptivity. Based on this, the methods to be developed are evaluated in the context of a practice-relevant case study.

Co-Operation Partner

Project Members

Zusatzinformationen / Extras

Quick Access:

Schnellnavigation zur Seite über Nummerneingabe