On the correctness of upper layers of automotive systems |
| |
Authors: | Jewgenij Botaschanjan Manfred Broy Alexander Gruler Alexander Harhurin Steffen Knapp Leonid Kof Wolfgang Paul Maria Spichkova |
| |
Affiliation: | 1.Institut für Informatik,Technische Universit?t München,Garching bei München,Germany;2.Department of Computer Science,Saarland University,Saarbrücken,Germany |
| |
Abstract: | Formal verification of software systems is a challenge that is particularly important in the area of safety-critical automotive systems. Here, approaches like direct code verification are far too complicated, unless the verification is restricted to small textbook examples. Furthermore, the verification of application logic is of limited use in industrial context, unless the underlying operating system and the hardware are verified, too. This paper introduces a generic model stack, allowing the verification of all system layers as well as the concrete application models being used in the upper layers. The presented models and proofs close the gap between the correctness proof for the lower layers of car electronics developed at the Saarland University and the verification procedure for distributed applications developed at the Technische Universität München. |
| |
Keywords: | Formal verification Automotive software Model-based development Time-triggered systems |
本文献已被 SpringerLink 等数据库收录! |
|