În informatică și ingineria software, metodele formale sunt un grup de tehnici bazate pe un aparat matematic pentru specificarea , dezvoltarea și verificarea software - ului și hardware -ului [1] . Utilizarea metodelor formale pentru proiectarea software-ului și hardware-ului se datorează așteptării că, ca și în alte domenii de inginerie, utilizarea analizei matematice poate crește semnificativ fiabilitatea sistemelor [2] . În același timp, metodele formale sunt destul de complexe, necesită pregătire specială, investiții de timp și resurse și se bazează adesea pe presupuneri care nu sunt întotdeauna realizabile în condiții reale. Acest lucru duce la faptul că metodele formale sunt cel mai des folosite în proiectarea sistemelor de înaltă precizie, unde importanța siguranței justifică orice mijloace.
Metodele formale se ocupă de aplicarea unei clase destul de largi de tehnici fundamentale ale informaticii teoretice : diverse calcule ale logicii , limbaje formale , teoria automatelor , semantică formală , sisteme de tip și tipuri de date algebrice [3] .
Există trei niveluri de aplicare a metodelor formale:
Nivel zero Se dezvoltă o specificație formală , apoi se scrie codul programului uitându-se la ea. În acest caz, diferența dintre partea formală și cea informală rămâne nedovedită, dar soluția poate fi rentabilă. Primul nivel Codul programului este derivat din specificația formală în mod automat, sunt utilizate mecanisme de verificare și sunt dovedite cele mai critice proprietăți ale sistemului. Această cale este adesea aleasă pentru sisteme de înaltă precizie. Al doilea nivel Demonstratorii automati de teoreme sunt utilizați pentru a obține dovezi complet formalizate care sunt verificate automat. Abordarea necesită multă investiție și cercetare, dar dă roade în părțile cele mai critice ale sistemelor complexe unde erorile nu sunt permise (de exemplu, în proiectarea circuitelor integrate ).Abordările metodologice formale pot fi, de asemenea, clasificate într-un mod similar cu semantica formală a limbajelor de programare :
Semantică denotațională _ _ _ Semnificația unui sistem este exprimată în termeni de mulțimi parțial ordonate , iar metodele se bazează pe o teorie bine dezvoltată în jurul lor. Limitarea metodei este că nu orice sistem poate fi considerat intuitiv sau natural ca o funcție . Semantică operațională _ _ _ Valoarea unui sistem este indicată printr-o succesiune de acțiuni în cadrul unui model de calcul mai simplu (cum ar fi calculul lambda sau rețelele Petri ). Metodele sunt renumite pentru simplitatea lor, dacă nu subliniate prin faptul că se bazează pe semantica unui sistem „mai simplu”, care trebuie și el definit prin ceva. Semantică axiomatică _ _ _ Semnificația sistemului este definită în termeni de precondiții și postcondiții , ceea ce face posibilă conectarea teoriei cu logica clasică, dar nu oferă o idee despre ceea ce se întâmplă exact în interiorul sistemului (cum se realizează postcondițiile pe baza condițiilor preliminare) .În plus, adesea se pot obține rezultate dramatic pozitive prin sacrificarea aplicabilității globale și a supraformalizării - astfel de cazuri sunt numite metode formale „ușoare” (ușoare). Ele pot fi împărțite în două tipuri: cu automatizare îmbunătățită și cu automatizare slăbită. Un exemplu de automatizare îmbunătățită este analizatorul de specificații Alloy Analyzer , care, pentru a reduce problema găsirii unui model la unul rezolvabil, restrângând zona de căutare (în consecință, Alloy funcționează complet automat, spre deosebire de probatorii interactivi, dar are o șansa de a nu găsi unele probleme). Un exemplu de una slăbită este convergența gramaticilor , în care imposibilitatea de rezolvare a problemei echivalenței a două limbaje formale este gestionată de faptul că transformările sunt efectuate de persoana însăși, iar concluziile sunt deja trase din proprietăți. a operatorilor folositi de acesta.
Metodele formale sunt aplicate în diferite etape ale dezvoltării software :
Specificație Cu ajutorul metodelor formale, este posibil să descrieți viitorul sistem cu orice nivel de detaliu. O astfel de descriere formală poate fi utilizată în mod direct sau indirect în avantaj în etapele ulterioare. În același timp, lucrul pentru demonstrarea unui număr de proprietăți funcționale necesare poate începe imediat și poate merge în paralel cu scrierea sau generarea codului. Există o serie de limbaje și calcule pentru specificațiile formale, dar niciunul nu poate pretinde că este la fel de universal ca forma Backus-Naur pentru specificarea sintaxelor . Dezvoltare Dacă o specificație formală folosește semantică operațională, comportamentul observat al unui anumit sistem poate fi comparat cu comportamentul așteptat, deoarece o astfel de semantică poate fi fezabilă și poate fi chiar folosită pentru generarea automată a codului. Dacă se folosește semantica axiomatică, atunci precondițiile și postcondițiile se pot mapa direct la instrucțiunile din codul executabil. Verificare Odată ce o specificație formală a fost pregătită, aceasta poate fi utilizată pentru a demonstra proprietățile necesare. Verificarea poate fi deductivă și model : deductivă folosește demonstrarea automată a teoremelor sau algebrelor specifice , iar modelul își bazează concluziile nu pe sistemul în sine, ci pe modelul construit pe acesta [4] . În același timp, nu este absolut necesar să construiți manual modelul, dacă sunt aplicabile tehnici precum secțiunea programului .Dovezile manuale necesită o investiție semnificativă de resurse și nu oferă niciun beneficiu decât confirmarea corectitudinii. Ca urmare, metodele formale sunt utilizate fie în zonele în care dovezile pot fi obținute automat prin software, fie în cele în care costul erorii este prea mare (de exemplu, la crearea unei nave spațiale sau a imagisticii prin rezonanță magnetică ).
| Dezvoltare de software | |
|---|---|
| Proces | |
Concepte de nivel înalt | |
| Directii |
|
| Metodologii de dezvoltare | |
| Modele |
|
Cifre notabile |
|