About: A Road to a Formally Verified General-Purpose Operating System     Goto   Sponge   NotDistinct   Permalink

An Entity of Type : http://linked.opendata.cz/ontology/domain/vavai/Vysledek, within Data Space : linked.opendata.cz associated with source document(s)

AttributesValues
rdf:type
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. (en)
Title
  • A Road to a Formally Verified General-Purpose Operating System
  • A Road to a Formally Verified General-Purpose Operating System (en)
skos:prefLabel
  • A Road to a Formally Verified General-Purpose Operating System
  • A Road to a Formally Verified General-Purpose Operating System (en)
skos:notation
  • RIV/00216208:11320/10:10002270!RIV11-MSM-11320___
http://linked.open...avai/riv/aktivita
http://linked.open...avai/riv/aktivity
  • Z(MSM0021620838)
http://linked.open...iv/cisloPeriodika
  • 6150
http://linked.open...vai/riv/dodaniDat
http://linked.open...aciTvurceVysledku
http://linked.open.../riv/druhVysledku
http://linked.open...iv/duvernostUdaju
http://linked.open...titaPredkladatele
http://linked.open...dnocenehoVysledku
  • 244943
http://linked.open...ai/riv/idVysledku
  • RIV/00216208:11320/10:10002270
http://linked.open...riv/jazykVysledku
http://linked.open.../riv/klicovaSlova
  • HelenOS; formal verification; operating systems (en)
http://linked.open.../riv/klicoveSlovo
http://linked.open...odStatuVydavatele
  • DE - Spolková republika Německo
http://linked.open...ontrolniKodProRIV
  • [2D060F9FB46A]
http://linked.open...i/riv/nazevZdroje
  • Lecture Notes in Computer Science
http://linked.open...in/vavai/riv/obor
http://linked.open...ichTvurcuVysledku
http://linked.open...cetTvurcuVysledku
http://linked.open...UplatneniVysledku
http://linked.open...v/svazekPeriodika
  • 2010
http://linked.open...iv/tvurceVysledku
  • Děcký, Martin
http://linked.open...n/vavai/riv/zamer
issn
  • 0302-9743
number of pages
http://localhost/t...ganizacniJednotka
  • 11320
is http://linked.open...avai/riv/vysledek of
Faceted Search & Find service v1.16.118 as of Jun 21 2024


Alternative Linked Data Documents: ODE     Content Formats:   [cxml] [csv]     RDF   [text] [turtle] [ld+json] [rdf+json] [rdf+xml]     ODATA   [atom+xml] [odata+json]     Microdata   [microdata+json] [html]    About   
This material is Open Knowledge   W3C Semantic Web Technology [RDF Data] Valid XHTML + RDFa
OpenLink Virtuoso version 07.20.3240 as of Jun 21 2024, on Linux (x86_64-pc-linux-gnu), Single-Server Edition (126 GB total memory, 58 GB memory in use)
Data on this page belongs to its respective rights holders.
Virtuoso Faceted Browser Copyright © 2009-2024 OpenLink Software