Inden for datalogi og softwareteknik er formelle metoder en gruppe af teknikker baseret på et matematisk apparat til specifikation , udvikling og verifikation af software og hardware [1] . Anvendelsen af formelle metoder til design af software og hardware skyldes forventningen om, at brugen af matematisk analyse som på andre ingeniørområder kan øge systemernes pålidelighed væsentligt [2] . Samtidig er formelle metoder ret komplekse, kræver særlig uddannelse, tids- og ressourceinvesteringer og er ofte baseret på antagelser, der ikke altid er opnåelige under reelle forhold. Dette fører til, at formelle metoder oftest anvendes ved design af højpræcisionssystemer, hvor vigtigheden af sikkerhed retfærdiggør ethvert middel.
Formelle metoder beskæftiger sig med anvendelsen af en ret bred klasse af grundlæggende teknikker inden for teoretisk datalogi : forskellige logiske beregninger , formelle sprog , automatteori , formel semantik , typesystemer og algebraiske datatyper [3] .
Der er tre niveauer for anvendelse af formelle metoder:
Nul niveau Der udvikles en formel specifikation , hvorefter programkoden skrives og kigger på den. I dette tilfælde forbliver kløften mellem den formelle og uformelle del ubevist, men løsningen kan være omkostningseffektiv. Første niveau Programkoden udledes automatisk fra den formelle specifikation , verifikationsmekanismer bruges , og systemets mest kritiske egenskaber bevises. Denne vej vælges ofte til højpræcisionssystemer. Andet niveau Automatiske teorembeviser bruges til at udlede fuldt formaliserede beviser, der automatisk verificeres. Tilgangen kræver mange investeringer og forskning, men betaler sig i de mest kritiske dele af komplekse systemer, hvor fejl ikke er tilladt (for eksempel i design af integrerede kredsløb ).Formelle metodetilgange kan også klassificeres på samme måde som programmeringssprogs formelle semantik :
Denotationel semantik _ _ _ Betydningen af et system udtrykkes i form af delvist ordnede sæt , og metoderne er afhængige af veludviklet teori omkring dem. Begrænsningen ved metoden er, at ikke alle systemer intuitivt eller naturligt kan betragtes som en funktion . Operationel semantik _ _ _ Værdien af et system er angivet ved en sekvens af handlinger inden for en enklere beregningsmodel (såsom lambda-regningen eller Petri nets ). Metoder er berygtet for deres enkelhed, hvis ikke understreget på det faktum, at de er afhængige af semantikken i et "simpelere" system, som også skal defineres gennem noget. Aksiomatisk semantik _ _ _ Systemets betydning er defineret i forhold til forudsætninger og postbetingelser , hvilket gør det muligt at forbinde teorien med klassisk logik, men giver ikke en idé om, hvad der præcist sker inde i systemet (hvordan postbetingelser opnås ud fra forudsætninger) .Derudover kan der ofte opnås dramatisk positive resultater ved at ofre global anvendelighed og overformalisering - sådanne sager kaldes "lette" (lette) formelle metoder. De kan opdeles i to typer: med forbedret og med svækket automatisering. Et eksempel på forbedret automatisering er specifikationsanalysatoren Alloy Analyzer , som for at reducere problemet med at finde en model til en løsning, der kan løses, indsnævrer søgeområdet (som følge heraf arbejder Alloy fuldautomatisk, i modsætning til interaktive testere, men har en chance for ikke at finde nogle problemer). Et eksempel på en svækket er konvergensen af grammatikker , hvor uløseligheden af problemet med ækvivalens af to formelle sprog styres af det faktum, at transformationerne udføres af personen selv, og konklusioner er allerede draget fra egenskaberne af de operatører, han bruger.
Formelle metoder anvendes på forskellige stadier af softwareudvikling :
Specifikation Ved hjælp af formelle metoder er det muligt at beskrive det fremtidige system med enhver detaljegrad. En sådan formel beskrivelse kan med fordel anvendes direkte eller indirekte på senere stadier. Samtidig kan arbejdet med at bevise en række nødvendige funktionelle egenskaber begynde med det samme og gå sideløbende med skrivning eller generering af kode. Der er en række sprog og calculi til formelle specifikationer, men ingen kan hævde at være så universel som Backus-Naur-formen til syntaksspecifikation . Udvikling Hvis en formel specifikation bruger operationel semantik, kan den observerede adfærd af et bestemt system sammenlignes med den forventede adfærd, fordi sådan semantik kan være gennemførlig og kan endda bruges til automatisk kodegenerering. Hvis der bruges aksiomatisk semantik, så kan forudsætninger og postbetingelser knyttes direkte til udsagn i eksekverbar kode. Verifikation Når en formel specifikation er udarbejdet, kan den bruges til at bevise de nødvendige egenskaber. Verifikation kan være deduktiv og model : deduktiv bruger automatisk bevis for sætninger eller specifikke algebraer , og model baserede sine konklusioner ikke på selve systemet, men på modellen bygget på det [4] . Samtidig er det absolut ikke nødvendigt at bygge modellen manuelt, hvis teknikker som programafsnit .Manuelle beviser kræver en betydelig investering af ressourcer og giver ingen andre fordele end bekræftelse af rigtigheden. Som et resultat heraf bruges formelle metoder enten i områder, hvor beviser kan opnås automatisk ved hjælp af software, eller i dem, hvor fejlomkostningerne er for høje (for eksempel ved oprettelse af rumfartøjer eller magnetisk resonansbilleddannelse ).
| Softwareudvikling | |
|---|---|
| Behandle | |
Koncepter på højt niveau | |
| Vejbeskrivelse |
|
| Udviklingsmetoder _ | |
| Modeller | |
| Bemærkelsesværdige tal |
|