NASA Logo

NTRS

NTRS - NASA Technical Reports Server

Collections About News Help Login

Due to the lapse in federal government funding, NASA is not updating this website. We sincerely regret this inconvenience.

Back to Results
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)
Shadrin, Andrey (Saarland Univ. Saarbruecken, Germany)
Tverdyshev, Sergey (Saarland Univ. Saarbruecken, Germany)
Date Acquired
August 24, 2013
Publication Date
April 1, 2010
Publication Information
Publication: Proceedings of the Second NASA Formal Methods Symposium
Subject Category
Mathematical And Computer Sciences (General)
Meeting Information
Meeting: NASA Formal Methods Symposium
Location: Washington D.C.
Country: United States
Start Date: April 13, 2010
End Date: April 15, 2010
Sponsors: NASA Headquarters
Funding Number(s)
CONTRACT_GRANT: BMBF01ISC38
Distribution Limits
Public
Copyright
Public Use Permitted.

Related Records

IDRelationTitle20100018529Collected WorksProceedings of the Second NASA Formal Methods Symposium20100018529Collected WorksProceedings of the Second NASA Formal Methods Symposium
No Preview Available