A számítástechnikában és a szoftverfejlesztésben a formális módszerek a szoftverek és hardverek specifikációjára , fejlesztésére és ellenőrzésére szolgáló matematikai apparátuson alapuló technikák csoportja [1] . A formális módszerek alkalmazása a szoftverek és hardverek tervezésénél abból az elvárásból fakad, hogy más mérnöki területekhez hasonlóan a matematikai elemzés alkalmazása jelentősen növelheti a rendszerek megbízhatóságát [2] . Ugyanakkor a formális módszerek meglehetősen összetettek, speciális képzést, idő- és erőforrás-befektetést igényelnek, és gyakran olyan feltételezéseken alapulnak, amelyek nem mindig valós körülmények között teljesíthetők. Ez oda vezet, hogy a formális módszereket leggyakrabban a nagy pontosságú rendszerek tervezésénél alkalmazzák, ahol a biztonság fontossága bármilyen eszközt indokol.
A formális módszerek az elméleti számítástechnika alapvető technikáinak meglehetősen széles osztályának alkalmazására vonatkoznak : különböző logikai számítások , formális nyelvek , automataelmélet , formális szemantika , típusrendszerek és algebrai adattípusok [3] .
A formális módszerek alkalmazásának három szintje van:
Nulla szint Kidolgozunk egy formális specifikációt , majd ránézve megírjuk a programkódot . Ebben az esetben a formális és az informális rész közötti szakadék nem bizonyított, de a megoldás költséghatékony lehet. Első szint A programkódot a formális specifikációból automatikusan levezetjük, ellenőrző mechanizmusokat alkalmazunk , és bizonyítjuk a rendszer legkritikusabb tulajdonságait. Ezt az utat gyakran választják nagy pontosságú rendszerek esetén. Második szint Az automatikus tételbizonyítókat teljesen formalizált bizonyítások származtatására használják, amelyek automatikusan ellenőrzöttek. A megközelítés sok befektetést és kutatást igényel, de megtérül az összetett rendszerek legkritikusabb részein, ahol a hibák nem megengedettek (például integrált áramkörök tervezésénél ).A formális módszertani megközelítések a programozási nyelvek formális szemantikájához hasonlóan osztályozhatók :
Denotációs szemantika _ _ _ Egy rendszer jelentése részben rendezett halmazokban fejeződik ki , és a módszerek a körülöttük lévő jól kidolgozott elméletre támaszkodnak. A módszer korlátja, hogy nem minden rendszer tekinthető intuitív módon vagy természetesen függvénynek . Műveleti szemantika _ _ _ Egy rendszer értékét egy egyszerűbb számítási modellen belüli műveletek sorozata jelöli (például a lambda-számítás vagy a Petri-háló ). A módszerek az egyszerűségükről híresek, ha nem az a tény hangsúlyozza, hogy egy „egyszerűbb” rendszer szemantikájára támaszkodnak, amelyet szintén meg kell határozni valamin keresztül. Axiomatikus szemantika _ _ _ A rendszer jelentése elő- és utófeltételekben van meghatározva , ami lehetővé teszi az elmélet összekapcsolását a klasszikus logikával, de nem ad képet arról, hogy pontosan mi történik a rendszeren belül (hogyan érhetők el az előfeltételek alapján az utófeltételek ) .Emellett gyakran drámaian pozitív eredményeket lehet elérni a globális alkalmazhatóság feláldozásával és a túlzott formalizálással – az ilyen eseteket "könnyű" (könnyű) formális módszereknek nevezik. Két típusra oszthatók: továbbfejlesztett és gyengített automatizálású. A továbbfejlesztett automatizálásra példa az Alloy Analyzer specifikációelemző, amely a modell megtalálásának problémáját megoldhatóra csökkenti, szűkíti a keresési területet (ennek eredményeként az Alloy teljesen automatizáltan működik, ellentétben az interaktív próbákkal, de rendelkezik egy annak esélye, hogy nem találnak bizonyos problémákat). A gyengítettre példa a nyelvtanok konvergenciája , amelyben két formális nyelv ekvivalenciájának problémájának megoldhatatlanságát az a tény kezeli, hogy a transzformációkat maga az ember hajtja végre, és a tulajdonságokból már levonják a következtetéseket. az általa használt operátorok közül.
A formális módszereket a szoftverfejlesztés különböző szakaszaiban alkalmazzák :
Leírás Formális módszerek segítségével bármilyen részletességgel leírható a leendő rendszer. Egy ilyen formális leírás közvetlenül vagy közvetve előnyösen felhasználható a későbbi szakaszokban. Ugyanakkor azonnal megkezdődhet számos szükséges funkcionális tulajdonság bizonyítása, amely párhuzamosan zajlik a kód írásával vagy generálásával. Számos nyelv és számítás létezik a formális specifikációkhoz, de egyik sem állíthatja, hogy olyan univerzális, mint a Backus-Naur formája a szintaktikai specifikációhoz . Fejlődés Ha egy formális specifikáció operatív szemantikát használ, akkor egy adott rendszer megfigyelt viselkedése összehasonlítható a várt viselkedéssel, mert az ilyen szemantika megvalósítható, sőt automatikus kódgenerálásra is használható. Ha axiomatikus szemantikát használunk, akkor az elő- és utófeltételek közvetlenül leképezhetnek a végrehajtható kódban lévő utasításokra . Igazolás A formális specifikáció elkészítése után a szükséges tulajdonságok bizonyítására használható. A verifikáció lehet deduktív és modell : a deduktív tételek vagy meghatározott algebrák automatikus bizonyítását használja , és a modell következtetéseit nem magára a rendszerre, hanem az arra épülő modellre alapozta [ 4] . Ugyanakkor egyáltalán nem szükséges manuálisan felépíteni a modellt, ha olyan technikák alkalmazhatók, mint a programrész .A kézi bizonyítások jelentős erőforrás-befektetést igényelnek, és a helyesség megerősítésén kívül nem járnak más előnnyel. Ennek eredményeként formális módszereket alkalmaznak azokon a területeken, ahol a bizonyítékok automatikusan beszerezhetők szoftveresen, vagy azokon, ahol a hiba költsége túl magas (például űrhajók vagy mágneses rezonancia képalkotás létrehozásakor ).
| Szoftverfejlesztés | |
|---|---|
| Folyamat | |
| Magas szintű koncepciók | |
| Útvonalak |
|
Fejlesztési módszertanok | |
| Modellek |
|
| Figyelemre méltó alakok |
|