Towards the Formal Verification of a Distributed Real-Time Automotive System
Erik Endres, Christian Mueller, Andrey Shadrin, Sergey Tverdyshev · 2010
We 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). 1