Third IEEE International Conference on Software Engineering and Formal Methods (SEFM'05) (2009)
Nov. 23, 2009 to Nov. 27, 2009
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/SEFM.2009.14
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.
Real-Time Operating System, Pervasive Verification, Refinement Proof, C Code Verification
N. W. Schirmer, M. Daum and M. Schmidt, "Implementation Correctness of a Real-Time Operating System," 2009 7th IEEE International Conference on Software Engineering and Formal Methods (SEFM 2009)(SEFM), Hanoi, 2009, pp. 23-32.