Formální metody - Formal methods

Ve vědě o počítačích , konkrétně softwarového inženýrství a hardware strojírenství , formální metody jsou zvláštní druh matematicky přesných technik pro specifikaci , vývoj a ověření všech softwarových a hardwarových systémů. Použití formálních metod pro návrh softwaru a hardwaru je motivováno očekáváním, že stejně jako v jiných technických oborech může provedení vhodné matematické analýzy přispět ke spolehlivosti a robustnosti návrhu.

Formální metody lze nejlépe popsat jako aplikaci poměrně široké škály základů teoretické informatiky , zejména logických kalkulů, formálních jazyků , teorie automatů , dynamického systému diskrétních událostí a sémantiky programu , ale také typových systémů a algebraických datových typů na problémy v softwaru a specifikace a ověření hardwaru.

Pozadí

Poloformální metody jsou formalismy a jazyky, které nejsou považovány za plně „ formální “. Odděluje úkol dokončit sémantiku do pozdější fáze, která se pak provádí buď lidskou interpretací, nebo interpretací prostřednictvím softwaru, jako jsou generátory kódu nebo testovacích případů.

Taxonomie

Formální metody lze použít na několika úrovních:

Úroveň 0: Lze provést formální specifikaci a poté z toho neformálně vytvořit program. Tomu se říká formální metody lite . V mnoha případech to může být nákladově nejefektivnější možnost.

Úroveň 1: Formální vývoj a formální ověření lze použít k vytvoření programu formálnějším způsobem. Mohou být například provedeny důkazy o vlastnostech nebo upřesnění ze specifikace na program. To může být nejvhodnější v systémech s vysokou integritou zahrnujících bezpečnost nebo zabezpečení .

Úroveň 2: Pro provádění plně formálních strojově kontrolovaných důkazů lze použít prověry věty . Navzdory vylepšování nástrojů a snižování nákladů to může být velmi nákladné a prakticky se to vyplatí, pouze pokud jsou náklady na chyby velmi vysoké (např. V kritických částech operačního systému nebo návrhu mikroprocesoru).

Další informace o tom jsou rozšířeny níže .

Stejně jako u sémantiky programovacího jazyka lze styly formálních metod zhruba klasifikovat následovně:

  • Denotační sémantika , ve které je význam systému vyjádřen v matematické teorii domén . Zastánci těchto metod spoléhají na dobře srozumitelnou povahu domén, které dávají systému smysl; kritici poukazují na to, že ne každý systém může být intuitivně nebo přirozeně vnímán jako funkce.
  • Operační sémantika , ve které je význam systému vyjádřen jako sled akcí (pravděpodobně) jednoduššího výpočetního modelu. Zastánci takových metod poukazují na jednoduchost svých modelů jako prostředek k expresivní jasnosti; kritici namítají, že problém sémantiky byl právě opožděn (kdo definuje sémantiku jednoduššího modelu?).
  • Axiomatická sémantika , ve které je význam systému vyjádřen pomocí předpokladů a postkondicionací, které jsou pravdivé před a po tom, co systém provede úkol. Zastánci si všímají spojení s klasickou logikou ; kritici poznamenávají, že taková sémantika nikdy ve skutečnosti nepopisuje, co systém dělá (pouze to, co je pravda před a po).

Lehké formální metody

Někteří praktici se domnívají, že komunita formálních metod příliš zdůraznila plnou formalizaci specifikace nebo designu. Tvrdí, že expresivita příslušných jazyků a složitost modelovaných systémů činí z plné formalizace obtížný a nákladný úkol. Jako alternativa byly navrženy různé lehké formální metody, které kladou důraz na částečnou specifikaci a cílenou aplikaci. Mezi příklady tohoto lehkého přístupu k formálním metodám patří zápis objektového modelování Alloy , Denneyova syntéza některých aspektů zápisu Z s vývojem řízeným použitím případu a nástroje CSK VDM .

Využití

Formální metody lze aplikovat na různých místech vývojového procesu .

Specifikace

K popisu systému, který má být vyvinut, mohou být použity formální metody na jakékoli požadované úrovni podrobností. Tento formální popis lze použít jako vodítko pro další vývojové činnosti (viz následující části); navíc jej lze použít k ověření, že požadavky na vyvíjený systém byly zcela a přesně specifikovány, nebo formalizaci systémových požadavků jejich vyjádřením ve formálním jazyce s přesnou a jednoznačně definovanou syntaxí a sémantikou.

Potřeba formálních specifikačních systémů se zaznamenává již roky. Ve zprávě ALGOL 58 John Backus představil formální notaci pro popis syntaxe programovacího jazyka, později pojmenovanou Backus normal form a poté přejmenovanou na Backus – Naur form (BNF). Backus také napsal, že formální popis významu syntakticky platných programů ALGOL nebyl dokončen včas pro zařazení do zprávy. „Formální zpracování sémantiky právních programů bude proto zahrnuto v dalším příspěvku.“ Nikdy se neobjevilo.

Rozvoj

Formální vývoj je použití formálních metod jako integrované součásti procesu vývoje systému podporovaného nástroji.

Jakmile byla vytvořena formální specifikace, může být specifikace použita jako vodítko při vývoji konkrétního systému během procesu návrhu (tj. Realizováno typicky v softwaru, ale potenciálně také v hardwaru). Například:

  • Pokud je formální specifikace v operační sémantice, lze pozorované chování konkrétního systému porovnat s chováním specifikace (která by sama měla být spustitelná nebo simulovatelná). Provozní příkazy specifikace mohou být navíc přístupné přímému překladu do spustitelného kódu.
  • Pokud je formální specifikace v axiomatické sémantice, předpoklady a postkondice specifikace se mohou stát tvrzeními ve spustitelném kódu.

Ověření

Formální ověření je použití softwarových nástrojů k prokázání vlastností formální specifikace nebo k prokázání, že formální model implementace systému splňuje její specifikaci.

Jakmile byla vyvinuta formální specifikace, může být specifikace použita jako základ pro prokázání vlastností specifikace (a doufejme, že odvozením vyvinutého systému).

Ověření odhlášení

Ověření odhlášení je použití vysoce důvěryhodného formálního ověřovacího nástroje. Takový nástroj může nahradit tradiční metody ověřování (nástroj může být dokonce certifikován).

Důkaz zaměřený na člověka

Někdy není motivací k prokázání správnosti systému zjevná potřeba ujištění o správnosti systému, ale touha lépe porozumět systému. V důsledku toho jsou některé důkazy o správnosti vytvářeny ve stylu matematického důkazu : ručně psané (nebo sazené) pomocí přirozeného jazyka , s použitím úrovně neformálnosti společné pro tyto důkazy. „Dobrý“ důkaz je ten, který je čitelný a srozumitelný ostatním lidským čtenářům.

Kritici takových přístupů poukazují na to, že nejednoznačnost vlastní přirozenému jazyku umožňuje v takovýchto důkazech odhalit chyby; v detailech nízké úrovně mohou být takové důkazy často přítomny jemné chyby. Práce vyžadující vytvoření tak dobrého důkazu navíc vyžadují vysokou úroveň matematické vyspělosti a odbornosti.

Automatický důkaz

Naproti tomu roste zájem o vytváření důkazů o správnosti takových systémů automatizovanými prostředky. Automatizované techniky spadají do tří obecných kategorií:

  • Automatizované dokazování teorémů , ve kterém se systém pokouší vytvořit formální důkaz od začátku, s popisem systému, sadou logických axiomů a sadou odvozovacích pravidel.
  • Kontrola modelu , ve které systém ověřuje určité vlastnosti pomocí vyčerpávajícího hledání všech možných stavů, do kterých by systém mohl během svého provádění vstoupit.
  • Abstraktní interpretace , ve které systém ověřuje přílišnou aproximaci behaviorální vlastnosti programu pomocí výpočtu fixního bodu přes (možná úplnou) mřížku, která ji reprezentuje.

Některé ověřovače automatizovaných teorémů vyžadují vedení ohledně toho, které vlastnosti jsou dostatečně „zajímavé“ pro sledování, zatímco jiné pracují bez lidského zásahu. Dáma modelu se může rychle zabřednout do kontroly milionů nezajímavých stavů, pokud nedostane dostatečně abstraktní model.

Zastánci takových systémů tvrdí, že výsledky mají větší matematickou jistotu než důkazy produkované lidmi, protože všechny nudné detaily byly algoritmicky ověřeny. Školení potřebné k používání takových systémů je také menší než školení potřebné k ručnímu vytváření dobrých matematických důkazů, díky čemuž jsou tyto techniky přístupné širšímu okruhu odborníků z praxe.

Kritici poznamenávají, že některé z těchto systémů jsou jako věštci : vyslovují pravdu, ale tuto pravdu nijak nevysvětlují. Existuje také problém „ ověření ověřovatele “; pokud je program, který pomáhá při ověřování, sám neprokázaný, může existovat důvod pochybovat o správnosti produkovaných výsledků. Některé moderní nástroje pro kontrolu modelů vytvářejí „zkušební protokol“, který podrobně popisuje každý krok v jejich důkazu, což umožňuje provádět s vhodnými nástroji nezávislé ověřování.

Hlavním rysem přístupu abstraktní interpretace je, že poskytuje zvukovou analýzu, tj. Nejsou vráceny žádné falešné negativy. Navíc je efektivně škálovatelný, vyladěním abstraktní domény představující analyzovanou vlastnost a použitím rozšiřujících operátorů k rychlé konvergenci.

Aplikace

Formální metody se používají v různých oblastech hardwaru a softwaru, včetně směrovačů, ethernetových přepínačů, směrovacích protokolů, bezpečnostních aplikací a mikrojader operačního systému, jako je seL4 . Existuje několik příkladů, ve kterých byly použity k ověření funkčnosti hardwaru a softwaru použitého v DC. Společnost IBM použila v procesu vývoje procesoru AMD x86 ACL2 , což je důkaz věty . Intel používá takové metody k ověření hardwaru a firmwaru (trvalý software naprogramovaný do paměti jen pro čtení). Centrum Dansk Datamatik použilo v 80. letech formální metody k vývoji kompilátorového systému pro programovací jazyk Ada, který se stal komerčním produktem s dlouhou životností.

Existuje několik dalších projektů NASA, ve kterých se uplatňují formální metody, jako například systém letecké dopravy příští generace , integrace bezpilotního letadlového systému do systému National Airspace System a Airborne Coordinated Conflict Resolution and Detection (ACCoRD). Metoda B s Atelierem B se používá k vývoji bezpečnostních automatismů pro různé podchody instalované po celém světě společnostmi Alstom a Siemens a také pro certifikaci Common Criteria a vývoj systémových modelů společností ATMEL a STMicroelectronics .

Formální ověření bylo v hardwaru často používáno většinou známých prodejců hardwaru, jako jsou IBM, Intel a AMD. Existuje mnoho oblastí hardwaru, ve kterých společnost Intel použila FM k ověření fungování produktů, jako je parametrizované ověření protokolu soudržného s mezipamětí, ověření jádra procesoru Intel Core i7 (pomocí dokazování vět , BDD a symbolického hodnocení), optimalizace pro architekturu Intel IA-64 využívající HOL light theorem prover a ověřování vysoce výkonného dvouportového gigabitového ethernetového řadiče s podporou protokolu PCI Express a technologií Intel Advanced Management pomocí Cadence. Podobně IBM použila formální metody při ověřování výkonových bran, registrů a funkčního ověřování mikroprocesoru IBM Power7.

Při vývoji softwaru

Při vývoji softwaru jsou formálními metodami matematické přístupy k řešení problémů softwaru (a hardwaru) na úrovni požadavků, specifikací a návrhu. Formální metody budou s největší pravděpodobností aplikovány na software a systémy kritické pro bezpečnost nebo zabezpečení, jako je například software pro avioniku . Standardy zajištění bezpečnosti softwaru, jako je DO-178C, umožňují použití formálních metod prostřednictvím doplňování a Common Criteria nařizuje formální metody na nejvyšších úrovních kategorizace.

Pro sekvenční software patří mezi příklady formálních metod B-metoda , specifikační jazyky používané v automatizovaném dokazování teorémů , RAISE a Z notace .

Ve funkčním programování , testování majetku na bázi umožnilo matematického popisu a testování (pokud není vyčerpávající testování) očekávaného chování jednotlivých funkcí.

Object Constraint Language (a specializace, jako je Java Modeling Language ) umožnila objektově orientované systémy, které mají být formálně specifikována, když ne nutně formálně ověřena.

U souběžného softwaru a systémů umožňují Petriho sítě , procesní algebry a stroje s konečným stavem (které jsou založeny na teorii automatů - viz také virtuální konečný stavový stroj nebo událostmi řízený konečný stavový stroj ) specifikaci spustitelného softwaru a lze je použít k vytvoření a ověření chování aplikace.

Dalším přístupem k formálním metodám při vývoji softwaru je napsat specifikaci v nějaké formě logiky-obvykle variaci logiky prvního řádu (FOL)-a poté přímo spustit logiku, jako by to byl program. OWL jazyk, založený na Popis Logic (DL), je příkladem. Pracuje se také na automatickém mapování některé verze angličtiny (nebo jiného přirozeného jazyka) do az logiky a na provádění logiky přímo. Příkladem jsou Attempto Controlled English a Internet Business Logic, které se nesnaží ovládat slovník nebo syntaxi. Funkce systémů, které podporují obousměrné mapování anglické logiky a přímé provádění logiky, spočívá v tom, že je lze vysvětlit jejich výsledky v angličtině na obchodní nebo vědecké úrovni.

Formální metody a zápisy

K dispozici je celá řada formálních metod a zápisů.

Specifikační jazyky

Dáma modelu

Hlavní článek: Seznam nástrojů pro kontrolu modelů
  • ESBMC
  • MALPAS Software Static Analysis Toolset -kontrola modelu průmyslové pevnosti používaná pro formální důkaz systémů kritických pro bezpečnost
  • PAT - bezplatná kontrola modelu, simulátor a kontrola upřesnění pro souběžné systémy a rozšíření CSP (např. Sdílené proměnné, pole, spravedlnost)
  • ROZTOČIT
  • UPPAAL

Organizace

Hlavní stránka: Kategorie: Organizace formálních metod

Viz také

Reference

Další čtení

externí odkazy

Archivní materiál