Implementation Correctness of a Real-Time Operating System

In the modern car, electronic devices are even employed for safety-critical missions like brake control, where failures might cost human lives. Among various approaches to increase the reliability of those devices, pervasive formal verification most securely rules out all systematic failures. The ma...

Full description

Saved in:
Bibliographic Details
Main Authors: Daum, M., Schirmer, N.W., Schmidt, M.
Format: Conference Proceeding
Language:English
Subjects:
Automotive engineering
C Code Verification
Communication system control
Computer science
Formal verification
Hardware
Operating systems
Pervasive Verification
Protocols
Real time systems
Real-Time Operating System
Refinement Proof
Software engineering
Software safety
Online Access:Request full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:In the modern car, electronic devices are even employed for safety-critical missions like brake control, where failures might cost human lives. Among various approaches to increase the reliability of those devices, pervasive formal verification most securely rules out all systematic failures. The main target of the Verisoft project is the development of technology for pervasive verification. Its application has been demonstrated in the automotive context by an exemplary distributed system consisting of hardware, a real-time operating system, and application programs. The contribution of this paper is a formal refinement proof linking an abstract specification of this real-time operating system to its C implementation.
ISSN:1551-0255
2160-7656
DOI:10.1109/SEFM.2009.14