V informatice a softwarovém inženýrství jsou formální metody skupinou technik založených na matematickém aparátu pro specifikaci , vývoj a ověřování softwaru a hardwaru [ 1] . Použití formálních metod pro návrh softwaru a hardwaru je způsobeno očekáváním, že stejně jako v jiných inženýrských oborech může použití matematické analýzy významně zvýšit spolehlivost systémů [2] . Formální metody jsou zároveň poměrně složité, vyžadují speciální školení, investice do času a zdrojů a často jsou založeny na předpokladech, které nejsou vždy dosažitelné v reálných podmínkách. To vede k tomu, že formální metody se nejčastěji používají při návrhu vysoce přesných systémů, kde důležitost bezpečnosti ospravedlňuje jakékoli prostředky.
Formální metody se zabývají aplikací poměrně široké třídy základních technik teoretické informatiky : různých logických kalkulů , formálních jazyků , teorie automatů , formální sémantiky , typových systémů a algebraických datových typů [3] .
Existují tři úrovně aplikace formálních metod:
Úroveň nula Je vyvinuta formální specifikace , poté je napsán programový kód , který se na ni dívá. V tomto případě zůstává mezera mezi formální a neformální částí neprokázaná, ale řešení může být nákladově efektivní. První úroveň Programový kód je odvozen z formální specifikace automaticky, jsou použity verifikační mechanismy a jsou prokázány nejkritičtější vlastnosti systému. Tato cesta se často volí u vysoce přesných systémů. Druhý stupeň Automatické dokazovatele vět se používají k odvození plně formalizovaných důkazů, které se automaticky ověřují. Tento přístup vyžaduje mnoho investic a výzkumu, ale vyplatí se v nejkritičtějších částech složitých systémů, kde nejsou povoleny chyby (například při návrhu integrovaných obvodů ).Formální metodické přístupy mohou být také klasifikovány podobným způsobem jako formální sémantika programovacích jazyků :
Denotační sémantika _ _ _ Význam systému je vyjádřen v podmínkách částečně uspořádaných množin a metody spoléhají na dobře rozvinutou teorii kolem nich. Omezením této metody je, že ne každý systém lze intuitivně nebo přirozeně považovat za funkci . Operační sémantika _ _ _ Hodnota systému je označena posloupností akcí v rámci jednoduššího výpočetního modelu (jako je lambda kalkul nebo Petriho sítě ). Metody jsou proslulé svou jednoduchostí, ne-li zdůrazněny tím, že se opírají o sémantiku „jednoduššího“ systému, který je také potřeba něčím definovat. Axiomatická sémantika _ _ _ Význam systému je definován z hlediska předpokladů a postpodmínek , což umožňuje propojit teorii s klasickou logikou, ale nedává představu o tom, co se přesně děje uvnitř systému (jak se dosahuje postpodmínek na základě předpokladů) .Navíc lze často dramaticky pozitivních výsledků dosáhnout obětováním globální použitelnosti a přílišnou formalizací – takové případy se nazývají „odlehčené“ (odlehčené) formální metody. Lze je rozdělit do dvou typů: se zesílenou a s oslabenou automatizací. Příkladem vylepšené automatizace je analyzátor specifikací Alloy Analyzer , který za účelem snížení problému s hledáním modelu na řešitelný, zužuje oblast hledání (v důsledku toho Alloy pracuje plně automatizovaně, na rozdíl od interaktivních dokazovačů, ale má šance, že nenajdete nějaké problémy). Příkladem oslabeného je konvergence gramatik , ve které je neřešitelnost problému ekvivalence dvou formálních jazyků řízena tím, že transformace provádí člověk sám a z vlastností jsou již vyvozovány závěry. jím používaných operátorů.
Formální metody se používají v různých fázích vývoje softwaru :
Specifikace Pomocí formálních metod je možné popsat budoucí systém s jakoukoliv úrovní detailů. Takovýto formální popis lze přímo nebo nepřímo s výhodou použít v pozdějších fázích. Práce na prokazování řady požadovaných funkčních vlastností přitom mohou začít okamžitě a jít souběžně s psaním či generováním kódu. Existuje řada jazyků a kalkulací pro formální specifikace, ale žádný nemůže tvrdit, že je tak univerzální jako formulář Backus-Naur pro specifikaci syntaxe . Rozvoj Pokud formální specifikace používá operační sémantiku, lze pozorované chování konkrétního systému porovnat s očekávaným chováním, protože taková sémantika může být proveditelná a může být dokonce použita pro automatické generování kódu. Pokud se použije axiomatická sémantika, pak se předběžné a následné podmínky mohou mapovat přímo na příkazy ve spustitelném kódu. Ověření Jakmile je připravena formální specifikace, lze ji použít k prokázání požadovaných vlastností. Verifikace může být deduktivní a modelová : deduktivní využívá automatický důkaz vět nebo specifických algeber a model nezakládá své závěry na systému samotném, ale na modelu na něm postaveném [4] . Zároveň není absolutně nutné sestavit model ručně, pokud jsou použitelné techniky jako programová sekce .Ruční nátisky vyžadují značné investice zdrojů a neposkytují žádnou jinou výhodu než potvrzení správnosti. V důsledku toho se formální metody používají buď v oblastech, kde lze důkazy získat automaticky pomocí softwaru, nebo v těch, kde je cena chyby příliš vysoká (například při vytváření kosmických lodí nebo zobrazování magnetickou rezonancí ).
| Vývoj softwaru | |
|---|---|
| Proces | |
Koncepty na vysoké úrovni | |
| Pokyny |
|
Vývojové metodiky | |
| Modelky |
|
| Pozoruhodné postavy |
|