Advertisement
Published in:
2010 | OriginalPaper | Chapter
From Operating-System Correctness to Pervasively Verified Applications
Authors : Matthias Daum, Norbert W. Schirmer, Mareike Schmidt
Published in: Integrated Formal Methods
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
Though program verification is known and has been used for decades, the verification 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.