Name
Abstract | ||
|---|---|---|
The tutorial reviews recent results from the Verisoft project [1]. We present a uniform mathematical theory, in which we can formulate pervasive correctness proofs for very large portions of automotive computer systems. The basic ingredients of this theory are (i)correctness of processors with memory mamagement units and external interrupts [2],(ii)correctness of a compiler for (a subset of) C [3], (iii)correctness of the generic multitasking operating system kernel CVM [4], (iv)formal modeling of I/O devices and correctness of drivers [5], (v)correctness of serial interfaces [6], (vi)clock synchronization [7,8], (vii)worst case execution time analysis using abstract interpretation [9]. Using ingredients (i), (iv), (v), and (vi) one can construct electronic control units (ECU) consisting of processors and interfaces to a FlexRay like bus [10]; timers on the ECUs are kept synchronized. An OSEKTime like real time operating system is derived from CVM [11]. The programming model for applications under this operating system is very simple: several (compiled) C programs run on each ECU in so called rounds under a fixed schedule. With the help of system calls the applications can update and poll a set of shared variables. The times for updating each shared variable are fixed by the schedule, too. An update to a shared variable in round k is visible to all application programs that poll this variable in round k+2. This programming model is very close to the model used in [12], where formal correctness proofs for a distributed emergency call application in cars are reported. Worst case timing analysis permits to guarantee, that applications and drivers satisfy the requirements of the schedule. If the requirements of the schedule are satisfied and the interfaces are programmed as prescribed by the schedule, then one can show that the user model is implememented by compiler, operating system and hardware [6]. An effort for the formal verification of all parts of the theory presented here is under way [13]. We report also on the status of this effort. |
Year | DOI | Venue |
|---|---|---|
2005 | 10.1007/11560548_3 | CHARME |
Keywords | Field | DocType |
pervasive correctness proof,generic multitasking operating system,formal correctness proof,operating system,pervasive verification,round k,automotive system,automotive computer system,shared variable,fixed schedule,programming model,real time operating system,electronic control unit,clock synchronization,formal verification,user model,timing analysis,satisfiability,worst case execution time | FlexRay,Programming language,Worst-case execution time,Programming paradigm,Computer science,Correctness,Real-time operating system,Compiler,Computer multitasking,Formal verification,Distributed computing | Conference |
Volume | ISSN | ISBN |
3725 | 0302-9743 | 3-540-29105-9 |
Citations | PageRank | References |
1 | 0.42 | 10 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Thomas In der Rieden | 1 | 22 | 1.70 |
| Dirk Leinenbach | 2 | 534 | 27.36 |
| Wolfgang J. Paul | 3 | 89 | 7.54 |