This HTML5 document contains 37 embedded RDF statements represented using HTML+Microdata notation.

The embedded RDF content will be recognized by any processor of HTML5 Microdata.

Namespace Prefixes

PrefixIRI
dctermshttp://purl.org/dc/terms/
n13http://localhost/temp/predkladatel/
n9http://linked.opendata.cz/resource/domain/vavai/riv/tvurce/
n16http://linked.opendata.cz/ontology/domain/vavai/
n7http://linked.opendata.cz/resource/domain/vavai/vysledek/RIV%2F00216208%3A11320%2F10%3A10002270%21RIV11-MSM-11320___/
n12http://linked.opendata.cz/resource/domain/vavai/zamer/
shttp://schema.org/
skoshttp://www.w3.org/2004/02/skos/core#
n3http://linked.opendata.cz/ontology/domain/vavai/riv/
n2http://linked.opendata.cz/resource/domain/vavai/vysledek/
rdfhttp://www.w3.org/1999/02/22-rdf-syntax-ns#
n15http://linked.opendata.cz/ontology/domain/vavai/riv/klicoveSlovo/
n5http://linked.opendata.cz/ontology/domain/vavai/riv/duvernostUdaju/
xsdhhttp://www.w3.org/2001/XMLSchema#
n18http://linked.opendata.cz/ontology/domain/vavai/riv/jazykVysledku/
n14http://linked.opendata.cz/ontology/domain/vavai/riv/aktivita/
n17http://linked.opendata.cz/ontology/domain/vavai/riv/druhVysledku/
n6http://linked.opendata.cz/ontology/domain/vavai/riv/obor/
n10http://reference.data.gov.uk/id/gregorian-year/

Statements

Subject Item
n2:RIV%2F00216208%3A11320%2F10%3A10002270%21RIV11-MSM-11320___
rdf:type
skos:Concept n16:Vysledek
dcterms:description
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 operating system 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 paper is the shift of focus from attempts to use a single %22silver-bullet%22 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 operating system. 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 operating system 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 paper is the shift of focus from attempts to use a single %22silver-bullet%22 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 operating system.
dcterms:title
A Road to a Formally Verified General-Purpose Operating System A Road to a Formally Verified General-Purpose Operating System
skos:prefLabel
A Road to a Formally Verified General-Purpose Operating System A Road to a Formally Verified General-Purpose Operating System
skos:notation
RIV/00216208:11320/10:10002270!RIV11-MSM-11320___
n3:aktivita
n14:Z
n3:aktivity
Z(MSM0021620838)
n3:cisloPeriodika
6150
n3:dodaniDat
n10:2011
n3:domaciTvurceVysledku
n9:3849775
n3:druhVysledku
n17:J
n3:duvernostUdaju
n5:S
n3:entitaPredkladatele
n7:predkladatel
n3:idSjednocenehoVysledku
244943
n3:idVysledku
RIV/00216208:11320/10:10002270
n3:jazykVysledku
n18:eng
n3:klicovaSlova
HelenOS; formal verification; operating systems
n3:klicoveSlovo
n15:formal%20verification n15:HelenOS n15:operating%20systems
n3:kodStatuVydavatele
DE - Spolková republika Německo
n3:kontrolniKodProRIV
[2D060F9FB46A]
n3:nazevZdroje
Lecture Notes in Computer Science
n3:obor
n6:IN
n3:pocetDomacichTvurcuVysledku
1
n3:pocetTvurcuVysledku
1
n3:rokUplatneniVysledku
n10:2010
n3:svazekPeriodika
2010
n3:tvurceVysledku
Děcký, Martin
n3:zamer
n12:MSM0021620838
s:issn
0302-9743
s:numberOfPages
17
n13:organizacniJednotka
11320