A számítástechnikában, különösen a szoftverfejlesztésben és a hardvertervezésben, a formális módszerek a szoftver- és hardverrendszerek specifikációjának, fejlesztésének és ellenőrzésének matematikailag szigorú technikáinak egy fajtáját jelentik. Ezek alkalmazását a szoftver- és hardvertervezésben az az elvárás motiválja, hogy más mérnöki tudományokhoz hasonlóan a megfelelő matematikai elemzések elvégzése hozzájárulhat a tervezés megbízhatóságához és robusztusságához.
A formális módszerek leginkább az elméleti számítástechnikai alapok széles skálájának alkalmazásaként írhatók le, különösen a logikai számítások, a formális nyelvek, az automataelmélet, a diszkrét eseménydinamikai rendszer és a programszemantika, de a típusrendszerek és algebrai adattípusok alkalmazása szoftveres problémákra. valamint hardverspecifikáció és ellenőrzés is ide tartozik.Monin, pp.3-4
Háttere A félig formális módszerek olyan formalizmusok és nyelvek, amelyek nem tekinthetők teljesen „formálisnak”. Egy későbbi szakaszra halasztja a szemantika kiegészítésének feladatát, amelyet aztán vagy emberi interpretáció, vagy szoftverek, például kód- vagy teszteset-generátorok segítségével hajtanak végre.
Taxonómia A formális módszerek számos szinten használhatók:
0. szint: A formális specifikáció elvégzése, majd ebből kidolgozni egy informális programot. Ezt a formális módszereket lite-nak nevezték el. Sok esetben ez lehet a legköltséghatékonyabb megoldás.
1. szint: A formális fejlesztés és ellenőrzés felhasználható a program formálisabb elkészítéséhez. Például elvégezhető a tulajdonságok bizonyítása, vagy a specifikációból egy program finomítása is. Ez lehet a legmegfelelőbb a nagy integritású, biztonsággal vagy védelemmel kapcsolatos rendszerekben.
2. szint: A tételbizonyítók teljesen formális, géppel ellenőrzött bizonyítások elvégzésére használhatók. A javuló eszközök és a csökkenő költségek ellenére ez nagyon drága megoldás lehet, és gyakorlatilag csak akkor éri meg, ha a hibák nagyon súlyosak (pl. az operációs rendszer vagy a mikroprocesszor tervezésének kritikus részein találhatóak).
A programozási nyelv szemantikájához hasonlóan a formális metódusok stílusai nagyjából a következők szerint osztályozhatók:
Denotációs szemantika: amelyben egy rendszer jelentését a tartományok matematikai elmélete fejezi ki. Az ilyen módszerek támogatói a tartományok jól érthető természetére hagyatkoznak, hogy jelentést adjanak a rendszernek. A kritikusok azonban rámutatnak arra, hogy nem minden rendszert lehet intuitívan vagy természetesen funkciónak tekinteni. Műveleti szemantika: amelyben egy rendszer jelentése egy (feltehetően) egyszerűbb számítási modell műveletsorozataként fejeződik ki. Az ilyen módszerek támogatói modelljeik egyszerűségére mutatnak rá, mint a kifejező világosság eszközére. A kritikusok azt állítják, hogy a szemantika problémája csak késett (de ki határozza meg az egyszerűbb modell szemantikáját?). Axiomatikus szemantika: amelyben a rendszer jelentését olyan elő- és utófeltételekkel fejezik ki, amelyek igazak a rendszer feladatának végrehajtása előtt és után is. A támogatók megjegyzik a kapcsolatot a klasszikus logikával; a kritikusok megjegyzik, hogy az ilyen szemantika sohasem írja le igazán, hogy egy rendszer mit csinál (csak azt, ami előtte és utána igaz).
Könnyű formális módszerek Egyes szakemberek úgy vélik, hogy a formális módszerek közössége túlhangsúlyozta egy specifikáció vagy terv teljes formalizálását.Daniel Jackson and Jeannette Wing, "Lightweight Formal Methods", IEEE Computer, April 1996Vinu George and Rayford Vaughn, "Application of Lightweight Formal Methods in Requirement Engineering" , Crosstalk: The Journal of Defense Software Engineering, January 2003 Azt állítják, hogy az érintett nyelvek kifejezőképessége, valamint a modellezett rendszerek összetettsége miatt a teljes formalizálás nehéz és költséges feladat. Alternatív megoldásként különféle könnyű formális módszereket javasoltak, amelyek a részleges specifikációt és a célzott alkalmazást hangsúlyozzák. A formális módszerek ilyen könnyű megközelítésére példák az Alloy objektummodellezési jelölés,Daniel Jackson, "Alloy: A Lightweight Object Modelling Notation", ACM Transactions on Software Engineering and Methodology (TOSEM), Volume 11, Issue 2 (April 2002), pp. 256-290 a Z jelölés egyes aspektusainak Denney-féle szintézise használati esetvezérelt fejlesztéssel,Richard Denney, Succeeding with Use Cases: Working Smart to Deliver Quality, Addison-Wesley Professional Publishing, 2005, . és a CSK VDM Tools.Sten Agerholm and Peter G. Larsen, "A Lightweight Approach to Formal Methods" , In Proceedings of the International Workshop on Current Trends in Applied Formal Methods, Boppard, Germany, Springer-Verlag, October 1998
Felhasználásuk A formális módszerek a fejlesztési folyamat különböző pontjain alkalmazhatók.
Specifikáció A formális módszerek használhatók a fejlesztendő rendszer leírására, függetlenül a kívánt részletességi szint(ek)től. Ez a formális leírás felhasználható a további fejlesztési tevékenységek irányítására (lásd a következő bekezdésekben). Ezen túlmenően ellenőrizhető, hogy a fejlesztés alatt álló rendszer követelményei teljesen és pontosan meg vannak-e határozva, vagy formalizálható a rendszerkövetelmények formális nyelven történő kifejezése, pontos és egyértelműen meghatározott szintaxissal és szemantikával.
A formális specifikációs rendszerek iránti igény évek óta megfigyelhető. Az ALGOL 58 jelentésben John Backus bemutatott egy formális jelölést a programozási nyelv szintaxisának leírására, amelyet később Backus normál alaknak, majd Backus–Naur formának (BNF) neveztek el.Knuth, Donald E. (1964), Backus Normal Form vs Backus Naur Form. Communications of the ACM, 7(12):735–736. Backus azt is írta, hogy a szintaktikailag érvényes ALGOL programok jelentésének formális leírása nem készült el időben ahhoz, hogy bekerüljön a jelentésbe. "Ezért a jogi programok szemantikájának formális kezelését egy későbbi írás tartalmazza majd." Soha nem jelent meg.
Fejlődés A formális fejlesztés a formális módszerek alkalmazása, az eszközökkel támogatott rendszerfejlesztési folyamat szerves részeként.
A formális specifikáció elkészítése után a specifikáció útmutatóként használható a konkrét rendszer fejlesztése során, a tervezési folyamat során (azaz jellemzően szoftveresen, de potenciálisan hardveresen is). Például:
Ha a formális specifikáció a műveleti szemantikában van, akkor a konkrét rendszer megfigyelt viselkedése összehasonlítható a specifikáció viselkedésével (,amelynek maga is végrehajthatónak vagy szimulálhatónak kell lennie). Ezenkívül a specifikáció műveleti parancsai alkalmasak lehetnek végrehajtható kódra történő közvetlen fordításra. Ha a formális specifikáció axiomatikus szemantikában van, akkor a specifikáció elő- és utófeltételei állításokká válhatnak a végrehajtható kódban.
Ellenőrzés A formális ellenőrzés szoftvereszközök használata egy formális specifikáció tulajdonságainak bizonyítására, vagy annak bizonyítására, hogy egy rendszermegvalósítás formális modellje megfelel a specifikációjának.
A formális specifikáció kidolgozása után a specifikáció alapul szolgálhat a specifikáció tulajdonságainak bizonyításához (és remélhetőleg a kifejlesztett rendszerre való következtetés útján).
A kijelentkezés ellenőrzése A kijelentkezési ellenőrzés egy hivatalos ellenőrző eszköz használata, amely nagyon megbízható. Egy ilyen eszköz helyettesítheti a hagyományos ellenőrzési módszereket (az eszköz akár tanúsított is lehet).
Ember által irányított bizonyíték Néha a rendszer helyességének bizonyítását nem az a nyilvánvaló igény, a rendszer helyességének megnyugtatása motiválja, hanem a rendszer könnyebb megérthetőségének a vágya. Következésképpen a helyesség bizonyos bizonyításait matematikai bizonyítási stílusban állítják elő: kézzel írva (vagy szedve) természetes nyelven, az ilyen bizonyításokra jellemző informalitási szinten. A „jó” bizonyíték az, amely más ember számára is olvasható és érthető.
Az ilyen megközelítések kritikusai rámutatnak arra, hogy a természetes nyelvben rejlő kétértelműség lehetővé teszi, hogy az ilyen bizonyításokban fel nem tárják a hibákat; gyakran kisebb hibák lehetnek az alacsony szintű részletekben, amelyeket az ilyen bizonyítások általában figyelmen kívül hagynak. Ezen túlmenően egy jó bizonyítás elkészítéséhez magasszintű matematikai kifinomultságot és szakértelmet igényel.
Automatizált bizonyítás Ezzel szemben egyre nagyobb az érdeklődés az ilyen rendszerek helyességének automatizált eszközökkel történő bizonyítása iránt. Az automatizált technikák három általános kategóriába sorolhatók:
Automatizált tételbizonyítás, amelyben a rendszer a semmiből próbál formális bizonyítást előállítani, a rendszer leírásával, logikai axiómák halmazával, és következtetési szabályokkal. Modellellenőrzés, amelyben a rendszer bizonyos tulajdonságokat ellenőriz az összes lehetséges állapot kimerítő keresésével, amelybe a rendszer a végrehajtása során beléphet. Absztrakt interpretáció, amelyben a rendszer a program egy viselkedési tulajdonságának túlzott közelítését ellenőrzi, fixpont számítást használva az azt reprezentáló (esetleg teljes) rácson/hálón.
Egyes automatizált tételbizonyítóknak útmutatásra van szükségük, hogy mely tulajdonságok elég „érdekesek” a folytatáshoz, míg mások emberi beavatkozás nélkül működnek. A modellellenőrzők gyorsan elakadhatnak több millió érdektelen állapot ellenőrzésében, ha nem kapnak kellően absztrakt modellt.
Az ilyen rendszerek támogatói azzal érvelnek, hogy az eredmények nagyobb matematikai bizonyossággal rendelkeznek, mint az ember által előállított bizonyítások, mivel minden unalmas részletet algoritmikusan ellenőriztek. Az ilyen rendszerek használatához szükséges képzés is rövidebb, mint a jó matematikai bizonyítások kézi előállításához szükségessé, így a technikák a szakemberek szélesebb köre számára érhetők el.
A kritikusok megjegyzik, hogy ezen rendszerek némelyike olyan, mint az orákulum: kimondják az igazságot, de nem adnak rá magyarázatot. Felmerül a „hitelesítő ellenőrzése” probléma is; ha az ellenőrzést segítő program nincs bizonyítva, okunk lehet kétségbe vonni a kapott eredmények megalapozottságát. Egyes modern modellellenőrző eszközök „ellenőrzési naplót” készítenek, amely részletezi a bizonyítás minden lépését, lehetővé téve a megfelelő eszközökkel független ellenőrzés elvégzését.
Az absztrakt értelmezési megközelítés fő jellemzője, hogy megalapozott elemzést ad, azaz nem ad vissza hamis negatívumot. Ezen túlmenően hatékonyan skálázható az elemezni kívánt tulajdonságot reprezentáló absztrakt tartomány hangolásával, valamint szélesítő operátorok alkalmazásával a gyors konvergencia elérése érdekében.
Alkalmazása A formális módszereket a hardver és a szoftver különböző területein alkalmazzák, beleértve a routereket, az Ethernet-switch-eket, a routing protokollokat, a biztonsági alkalmazásokat és az operációs rendszer mikrokerneleit, például a seL4-et. Számos példa van arra, hogy a DC-kben használt hardver és szoftver működőképességének ellenőrzésére használták őket. Az IBM az ACL2 tételt használta az AMD x86 processzor fejlesztési folyamatában. Az Intel ilyen módszereket használ a hardver és a firmware (csak olvasható memóriába programozott állandó szoftver) ellenőrzésére. A Dansk Datamatik Center formális módszereket használt az 1980-as években, hogy kifejlesszen egy fordítórendszert az Ada programozási nyelvhez, amely hosszú életű kereskedelmi termékké vált.