From Operating-System Correctness to Pervasively Veried Applications - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2010

From Operating-System Correctness to Pervasively Veried Applications

Résumé

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.
Fichier principal
Vignette du fichier
libolos104.pdf (274.89 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

inria-00524575 , version 1 (08-10-2010)

Identifiants

  • HAL Id : inria-00524575 , version 1

Citer

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⟩
151 Consultations
281 Téléchargements

Partager

Gmail Facebook X LinkedIn More