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.
Type de document :
Communication dans un congrès
Mery, Dominique and Merz, Stephan. Integrated Formal Methods - IFM 2010, Oct 2010, Nancy, France. Springer Berlin / Heidelberg, 6396, pp.105-120, 2010, Lecture Notes in Computer Science
Liste complète des métadonnées

Littérature citée [16 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00524575
Contributeur : Ist Inria Nancy Grand Est <>
Soumis le : vendredi 8 octobre 2010 - 11:13:05
Dernière modification le : mardi 31 octobre 2017 - 14:22:18
Document(s) archivé(s) le : jeudi 25 octobre 2012 - 16:41:03

Fichier

libolos104.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00524575, version 1

Collections

Citation

Matthias Daum, Norbert W. Schirmer, Mareike Schmidt. From Operating-System Correctness to Pervasively Veried Applications. Mery, Dominique and Merz, Stephan. Integrated Formal Methods - IFM 2010, Oct 2010, Nancy, France. Springer Berlin / Heidelberg, 6396, pp.105-120, 2010, Lecture Notes in Computer Science. 〈inria-00524575〉

Partager

Métriques

Consultations de la notice

177

Téléchargements de fichiers

145