Abstrakt
Metody formálního popisu a verifikace představují shůdnou cestu k dosažení fundamentálně bezchybného software. Jen malá část operačních systémů však byla v praxi formálně verifikována a to i přesto, že operační systémy tvoří kritickou součást téměř všech softwarových systémů.
Tento článek popisuje několik klíčových vlastností návrhu operačních systémů, které by měly umožnit zjednodušení formální verifikace, a popisuje aktuální postup prací a první pozorování formální verifikace systému HelenOS, což je moderní operační systém mikrojádrového typu, vyvýjený ovšem bez speciálního ohledu na budoucí formální verifikaci (takové ohledy jsou typicky velmi nákladné a časově náročné). Přínos tohoto článku je v posunu důrazu z univerzálního všeobjímajícího přístupu formální verifikace na použití vhodné kombinace různých formalismů a technik, které dohromady dovedou lépe pokrýt různé aspekty operačního systému.