Towards the Formal Verification of a Distributed Real-Time Automotive SystemWe present the status of a project which aims at building, formally and pervasively verifying a distributed automotive system. The target system is a gate-level model which consists of several interconnected electronic control units with independent clocks. This model is verified against the specification as seen by a system programmer. The automotive system is implemented on several FPGA boards. The pervasive verification is carried out using combination of interactive theorem proving (Isabelle/HOL) and model checking (LTL).
Document ID
20100018553
Acquisition Source
Langley Research Center
Document Type
Conference Paper
Authors
Endres, Erik (Saarland Univ. Saarbruecken, Germany)
Mueller, Christian (Saarland Univ. Saarbruecken, Germany)