loading...
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
2009 Seventh IEEE International Conference on Software Engineering and Formal Methods
Implementation Correctness of a Real-Time Operating System
Hanoi, Vietnam
November 23-November 27
ISBN: 978-0-7695-3870-9
ASCII Text
x 
 
Matthias Daum, Norbert W. Schirmer, Mareike Schmidt, "Implementation Correctness of a Real-Time Operating System," Software Engineering and Formal Methods, IEEE International Conference on, pp. 23-32, 2009 Seventh IEEE International Conference on Software Engineering and Formal Methods, 2009.
 
 
BibTex
x
 
@article{ 10.1109/SEFM.2009.14,
author = {Matthias Daum and Norbert W. Schirmer and Mareike Schmidt},
title = {Implementation Correctness of a Real-Time Operating System},
journal ={Software Engineering and Formal Methods, IEEE International Conference on},
volume = {0},
year = {2009},
isbn = {978-0-7695-3870-9},
pages = {23-32},
doi = {http://doi.ieeecomputersociety.org/10.1109/SEFM.2009.14},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
}
 
 
RefWorks Procite/RefMan/Endnote
x 
 
TY - CONF
JO - Software Engineering and Formal Methods, IEEE International Conference on
TI - Implementation Correctness of a Real-Time Operating System
SN - 978-0-7695-3870-9
SP23
EP32
A1 - Matthias Daum,
A1 - Norbert W. Schirmer,
A1 - Mareike Schmidt,
PY - 2009
KW - Real-Time Operating System
KW - Pervasive Verification
KW - Refinement Proof
KW - C Code Verification
VL - 0
JA - Software Engineering and Formal Methods, IEEE International Conference on
ER -
 
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.
Index Terms:
Real-Time Operating System, Pervasive Verification, Refinement Proof, C Code Verification
Citation:
Matthias Daum, Norbert W. Schirmer, Mareike Schmidt, "Implementation Correctness of a Real-Time Operating System," sefm, pp.23-32, 2009 Seventh IEEE International Conference on Software Engineering and Formal Methods, 2009
Usage of this product signifies your acceptance of the Terms of Use.