Model Transformations to Mitigate the Semantic Gap in Embedded Systems Verification

Abstract

The VATES project addresses the problem of verifying embedded software by employing a novel combination of methods that are well-established on the level of declarative models, in particular process-algebraic specifications, as well as of methods that work especially well on the level of executable code. Beginning with executable code, we (automatically) extract a model in the form of a processalgebraic system description formulated in Communicating Sequential Processes (CSP). For this low-level CSP description, we can prove that it refines a high-level CSP specification which was previously developed. To relate the (Low-Level Virtual Machine) LLVM code with the low-level CSP model we designed an operational semantics of LLVM. In ongoing work we investigate the extraction algorithm with respect to preservation of semantics. Thereby, we are finally able to prove that given LLVM code formally conforms to its high-level CSP-based specification. In this paper we give an overview of results of VATES so far and show that this approach has the potential to seamlessly integrate modeling, implementation, transformation and verification stages of embedded system development.