A Road to a Formally Verified General-Purpose Operating System
Identifikátory výsledku
Kód výsledku v IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216208%3A11320%2F10%3A10002270" target="_blank" >RIV/00216208:11320/10:10002270 - isvavai.cz</a>
Výsledek na webu
—
DOI - Digital Object Identifier
—
Alternativní jazyky
Jazyk výsledku
angličtina
Název v původním jazyce
A Road to a Formally Verified General-Purpose Operating System
Popis výsledku v původním jazyce
Methods of formal description and verification represent a viable way for achieving fundamentally bug-free software. However, in reality only a small subset of the existing operating systems were ever formally verified, despite the fact that an operatingsystem is a critical part of almost any other software system. This paper points out several key design choices which should make the formal verification of an operating system easier and presents a work-in-progress and initial experiences with formal verification of HelenOS, a state-of-the-art microkernel-based operating system, which, however, was not designed specifically with formal verification in mind, as this is mostly prohibitive due to time and budget constrains. The contribution of this paperis the shift of focus from attempts to use a single "silver-bullet" formal verification method which would be able to verify everything to a combination of multiple formalisms and techniques to successfully cover various aspects of the o
Název v anglickém jazyce
A Road to a Formally Verified General-Purpose Operating System
Popis výsledku anglicky
Methods of formal description and verification represent a viable way for achieving fundamentally bug-free software. However, in reality only a small subset of the existing operating systems were ever formally verified, despite the fact that an operatingsystem is a critical part of almost any other software system. This paper points out several key design choices which should make the formal verification of an operating system easier and presents a work-in-progress and initial experiences with formal verification of HelenOS, a state-of-the-art microkernel-based operating system, which, however, was not designed specifically with formal verification in mind, as this is mostly prohibitive due to time and budget constrains. The contribution of this paperis the shift of focus from attempts to use a single "silver-bullet" formal verification method which would be able to verify everything to a combination of multiple formalisms and techniques to successfully cover various aspects of the o
Klasifikace
Druh
J<sub>x</sub> - Nezařazeno - Článek v odborném periodiku (Jimp, Jsc a Jost)
CEP obor
IN - Informatika
OECD FORD obor
—
Návaznosti výsledku
Projekt
—
Návaznosti
Z - Vyzkumny zamer (s odkazem do CEZ)
Ostatní
Rok uplatnění
2010
Kód důvěrnosti údajů
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Údaje specifické pro druh výsledku
Název periodika
Lecture Notes in Computer Science
ISSN
0302-9743
e-ISSN
—
Svazek periodika
2010
Číslo periodika v rámci svazku
6150
Stát vydavatele periodika
DE - Spolková republika Německo
Počet stran výsledku
17
Strana od-do
—
Kód UT WoS článku
—
EID výsledku v databázi Scopus
—