Title: 
------
Verification of Distributed Embedded Real-Time Systems and Their 
Low-Level Implementations using Timed CSP

Abstract:
------------ 
Process calculi like Timed CSP offer a convenient level of abstraction 
for the specification and verification of distributed embedded 
real-time systems. Complex concurrent systems can be specified in 
terms of interacting modules whose interaction can be analyzed on the 
abstract level of the process calculus. However, the high level of 
abstraction introduces a semantic gap between the process algebraic 
specification and the final implementation given in a general purpose 
programming language.

In this talk, we present the theoretical concepts of a development 
and verification approach for distributed embedded real-time systems. 
In this approach, the goal is to formally verify that concrete 
implementations of individual system components conform to their 
respective Timed CSP specifications. The key idea underlying the 
presented approach is a formal relation between timed process 
algebraic specifications and their implementations given in the 
compiler intermediate language LLVM. To achieve this relation and 
enable its concrete application, we adapt the notion of weak timed 
bisimulation and provide a Hoare-calculus for the intermediate 
language. Using the presented relation, we are able to transfer 
system properties established on the abstract level of the process 
calculus to the low-level implementation. By formalizing the presented 
concepts in the Isabelle/HOL theorem prover, we are able to provide a 
mechanized and partly automatized proof environment.