Formális módszerek

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.

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. 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, a Z jelölés egyes aspektusainak Denney-féle szintézise használati esetvezérelt fejlesztéssel, és a CSK VDM Tools.

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. 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.

A NASA-nak számos más projektje is van, amelyekben formális módszereket alkalmaznak, mint például a következő generációs légi közlekedési rendszer, a Pilóta nélküli légijármű-rendszer integrációja a nemzeti légtérrendszerben, és a légi fedélzeti koordinált konfliktusmegoldás és észlelés(ACCoRD). A B-Method az Atelier B-vel biztonsági automatizmusok fejlesztésére szolgál az Alstom és a Siemens által világszerte telepített különféle metrókhoz, valamint a Common Criteria tanúsításhoz, az ATMEL és a STMicroelectronics rendszermodellek fejlesztéséhez.

A formális ellenőrzést a legtöbb jól ismert hardvergyártó, például az IBM, az Intel, és az AMD, gyakran alkalmazza a hardverben. A hardvernek számos olyan területe van, ahol az Intel FM-eket használt a termékek működésének ellenőrzésére, mint például a gyorsítótár-koherens protokoll paraméterezett ellenőrzése, Intel Core i7 processzor végrehajtó motor érvényesítése (tételbizonyítás, BDD-k, és szimbolikus kiértékelés), az Intel IA-64 architektúrához való optimalizálás a HOL fénytétel bizonyításával valamint a nagy teljesítményű, kétportos gigabites Ethernet-vezérlő ellenőrzése, amely támogatja a PCI expressz protokollt és az Intel Advanced Management technológiát a Cadence használatával. Hasonlóképpen, az IBM formális módszereket alkalmazott a teljesítménykapuk, regiszterek és az IBM Power7 mikroprocesszor funkcionális ellenőrzése során.

A szoftverfejlesztésben

A szoftverfejlesztésben a formális módszerek a szoftver (és a hardver) problémák megoldásának matematikai megközelítései a követelmények, a specifikáció és a tervezés szintjén. A formális módszereket leginkább a biztonság szempontjából kritikus vagy kritikus szoftverekre és rendszerekre, például repüléselektronikai szoftverekre alkalmazzák. A szoftverbiztonsági szabványok, mint például a DO-178C, lehetővé teszik a formális módszerek használatát kiegészítés útján, a Common Criteria pedig a formális módszereket írja elő a legmagasabb kategorizálási szinten.

A szekvenciális szoftvereknél a formális módszerek példái közé tartozik a B-method, az automatizált tételbizonyításban használt specifikációs nyelvek, a RAISE és a Z jelölés.

A funkcionális programozásban a tulajdonság-alapú tesztelés lehetővé tette az egyes függvények elvárt viselkedésének matematikai specifikációját és tesztelését (ha nem teljes körű tesztelést).

Az Object Constraint Language (és az olyan specializációk, mint a Java Modeling Language) lehetővé tették az objektumorientált rendszerek formális meghatározását, ha nem is feltétlenül hivatalosan ellenőrizték.

Párhuzamos szoftverek és rendszerek esetén a Petri-hálók, a folyamatalgebra és a véges állapotú gépek (,amelyek automata elméleten alapulnak – lásd még: virtuális véges állapotú gép vagy eseményvezérelt véges állapotú gép) lehetővé teszik a végrehajtható szoftverspecifikációt, és felépítésre és érvényesítésre használhatók. alkalmazási viselkedés.

A formális módszerek másik megközelítése a szoftverfejlesztésben az, hogy a logika valamilyen formájával – általában az elsőrendű logika (FOL) egy változatával – specifikációt írunk, majd közvetlenül végrehajtjuk a logikát, mintha az egy program lenne. Példa erre a leírási logikán (DL) alapuló OWL nyelv. Dolgoznak az angol (vagy más természetes nyelv) egyes verzióinak automatikus leképezésén is a logikához és a logikából, valamint a logika közvetlen végrehajtásán. Ilyen például az Attempto Controlled English és az Internet Business Logic, amelyek nem a szókincs vagy a szintaxis szabályozására törekszenek. A kétirányú angol-logikai leképezést és a logika közvetlen végrehajtását támogató rendszerek sajátossága, hogy eredményeiket angol nyelven üzleti vagy tudományos szinten is meg lehet magyarázni.

Formai módszerek és jelölések

Különféle formális módszerek és jelölések állnak rendelkezésre.

Specifikációs nyelvek

• Abstract State Machines (ASMs)
• A Computational Logic for Applicative Common Lisp (ACL2)
• Actor model
• Alloy
• ANSI/ISO C Specification Language (ACSL)
• Autonomic System Specification Language (ASSL)
• B-Method
• CADP
• Common Algebraic Specification Language (CASL)
• Esterel
• Java Modeling Language (JML)
• Knowledge Based Software Assistant (KBSA)
• Lustre
• mCRL2
• Perfect Developer
• Petri nets
• Predicative programming
• Process calculi
  • CSP
  • LOTOS
  • π-calculus
• RAISE
• Rebeca Modeling Language
• SPARK Ada
• Specification and Description Language
• TLA+
• USL
• VDM
  • VDM-SL
  • VDM++
• Z notation

Modellellenőrzők

• ESBMC
• MALPAS Software Static Analysis Toolset – an industrial-strength model checker used for formal proof of safety-critical systems
• PAT – a free model checker, simulator and refinement checker for concurrent systems and CSP extensions (e.g., shared variables, arrays, fairness)
• SPIN
• UPPAAL

Szervezetek

• APCB
• BCS-FACS
• Formal Methods Europe
• Z User Group

Fordítás

Ez a szócikk részben vagy egészben a Formal methods című angol Wikipédia-szócikk ezen változatának fordításán alapul. Az eredeti cikk szerkesztőit annak laptörténete sorolja fel. Ez a jelzés csupán a megfogalmazás eredetét és a szerzői jogokat jelzi, nem szolgál a cikkben szereplő információk forrásmegjelöléseként.

Kapcsolódó szócikkek

• Szerződésalapú programozás
• Logikai kalkulus

Források

• Jonathan P. Bowen and Michael G. Hinchey, Formal Methods. In Allen B. Tucker, Jr. (ed.), Computer Science Handbook, 2nd edition, Section XI, Software Engineering, Chapter 106, pages 106-1 – 106-25, Chapman & Hall / CRC Press, Association for Computing Machinery, 2004.
• Hubert Garavel (editor) and Susanne Graf. Formal Methods for Safe and Secure Computer Systems. Bundesamt für Sicherheit in der Informationstechnik, BSI study 875, Bonn, Germany, December 2013.
• The 2020 Expert Survey on Formal Methods, Formal Methods for Industrial Critical Systems: 25 International Conference, FMICS 2020, Lecture Notes in Computer Science (LNCS). Springer, 3–69. o.. DOI: 10.1007/978-3-030-58298-2_1 (2020. augusztus 29.). ISBN 978-3-030-58297-5 * Michael G. Hinchey, Jonathan P. Bowen, and Emil Vassev, Formal Methods. In Philip A. Laplante (ed.), Encyclopedia of Software Engineering, Taylor & Francis, 2010, pages 308–320.
• Marieke Huisman, Dilian Gurov, and Alexander Malkis, Formal Methods: From Academia to Industrial Practice – A Travel Guide, arXiv:2002.07279, 2020.
• (2020. szeptember 9.) „Formal methods in dependable systems engineering: a survey of professionals from Europe and North America”. Empirical Software Engineering 25 (6), 4473–4546. o, Kiadó: Springer Nature. DOI:10.1007/s10664-020-09836-5. 
• Jean François Monin and Michael G. Hinchey, Understanding formal methods, Springer, 2003, ISBN 1-85233-247-6.

További információk

• Formal Methods Europe (FME)
• Formal Methods Wiki
• Formal methods from Foldoc
• Formal method keyword on Microsoft Academic Search via Archive.org
• Evidence on Formal Methods uses and impact on Industry supported by the DEPLOY Archiválva 2012. június 8-i dátummal a Wayback Machine-ben project (EU FP7) in Archive.org