Skip to Main content Skip to Navigation
Conference papers

From Operating-System Correctness to Pervasively Veried Applications

Abstract : Though program verication is known and has been used for decades, the verication of a complete computer system still remains a grand challenge. Part of this challenge is the interaction of application programs with the operating system, which is usually entrusted with retrieving input data from and transferring output data to peripheral devices. In this scenario, the correct operation of the applications inherently relies on operating-system correctness. Based on the formal correctness of our real-time operating system Olos, this paper describes an approach to pervasively verify applications running on top of the operating system.
Complete list of metadata

Cited literature [16 references]  Display  Hide  Download

https://hal.inria.fr/inria-00524575
Contributor : Ist Inria Nancy Grand Est Connect in order to contact the contributor
Submitted on : Friday, October 8, 2010 - 11:13:05 AM
Last modification on : Thursday, June 4, 2020 - 6:24:02 PM
Long-term archiving on: : Thursday, October 25, 2012 - 4:41:03 PM

File

libolos104.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : inria-00524575, version 1

Collections

Citation

Matthias Daum, Norbert W. Schirmer, Mareike Schmidt. From Operating-System Correctness to Pervasively Veried Applications. Integrated Formal Methods - IFM 2010, INRIA Nancy Grand Est, Oct 2010, Nancy, France. pp.105-120. ⟨inria-00524575⟩

Share

Metrics

Record views

143

Files downloads

187