Verificarea formală a programului în practică

Voi încerca să dau un răspuns succint la unele dintre întrebările tale.Vă rugăm să rețineți că acesta nu este strict domeniul meu de cercetare, așa că unele dintre informațiile mele pot fi învechite / incorecte.

1. Există multe instrumente special concepute pentru a demonstra în mod formal proprietățile de Java și C ++.

   Cu toate acestea, trebuie să fac o mică digresiune aici: ce înseamnă să dovedesc corectitudinea unui program? Verificatorul de tip Java dovedește o proprietate formală a unui program Java, și anume că anumite erori, cum ar fi adăugarea unui float și a unui int, nu pot niciodată apar! Îmi imaginez că sunteți interesat de proprietăți mult mai puternice, și anume că programul dvs. nu poate intra niciodată într-o stare nedorită sau că ieșirea unei anumite funcții este conformă cu o anumită specificație matematică. Pe scurt, există un gradient larg de ceea ce poate însemna „dovedirea unui program corect”, de la proprietăți de securitate simple până la o dovadă completă a faptului că programul îndeplinește o specificație detaliată.

   Acum voi presupune că sunteți interesat să demonstrați proprietăți puternice despre programele dvs. Dacă sunteți interesat de proprietățile de securitate (programul dvs. poate nu ajunge la o anumită stare), atunci, în general, se pare că cea mai bună abordare este verificarea modelului . Cu toate acestea, dacă doriți să specificați complet comportamentul unui program Java, cel mai bun pariu este să utilizați un limbaj de specificare pentru acel limbaj, de exemplu JML . Există astfel de limbaje pentru specificarea comportamentului programelor C, de exemplu ACSL , dar nu știu despre C ++.

2. Odată ce aveți specificațiile, trebuie să demonstrați că programul este conform cu specificațiile respective.

   Pentru aceasta aveți nevoie de un instrument care are un înțelegerea formală a ambelor specificația dvs. și semantica operațională a limbajului dvs. (Java sau C ++) pentru a exprima teorema adecvării , și anume că execuția din program respectă specificațiile.

   Acest instrument ar trebui să vă permită, de asemenea, să formulați sau să generați dovada teoremei respective. Acum, ambele sarcini (specificarea și demonstrarea) sunt destul de dificile, deci sunt adesea separate în două:

   • Un instrument care analizează codul, specificația și generează teorema adecvării. După cum a menționat Frank, Krakatoa este un exemplu de astfel de instrument.

   • Un instrument care dovedește teorema ( s), automat sau interactiv. Coq interacționează cu Krakatoa în acest mod și există câteva instrumente automate puternice precum Z3 care pot fi, de asemenea, utilizate.

   Un punct (minor): există unele teoreme care sunt mult prea greu pentru a fi dovedite cu metode automate, iar probatorii de teoreme automate au ocazional erori de soliditate care îi fac mai puțin de încredere. Aceasta este o zonă în care Coq strălucește în comparație (dar nu este automat!).

3. Dacă doriți să generați cod Ocaml, atunci cu siguranță scrieți mai întâi în Coq (Gallina), apoi extrage codul. Cu toate acestea, Coq este groaznic când generează C ++ sau Java, dacă este chiar posibil.

4. Poate instrumentele de mai sus să rezolve problemele de filetare și de performanță? Probabil că nu, problemele legate de performanță și filetare sunt tratate cel mai bine prin instrumente special concepute, deoarece acestea sunt probleme deosebit de grele. Nu sunt sigur că am instrumente de recomandat aici, deși proiectul PolyNI al lui Martin Hofmann pare interesant.

În concluzie: verificarea formală a programelor Java și C ++ „din lumea reală” este un domeniu larg și bine dezvoltat, iar Coq este potrivit pentru părți din acea sarcină. Puteți găsi o prezentare generală la nivel înalt aici , de exemplu.

Comentarii

• Vă mulțumim pentru această postare și referințele pe care le-ați adăugat. IMHO, scopul inginerilor de software este să poată lansa rapid sisteme care 1) vor oferi întotdeauna rezultate corecte, 2) nu vor da greș niciodată. Aș putea vedea o problemă de regresie aici, unde ați putea dori să demonstrați că specificația în sine este ” fără bug ” 🙂 cum ar fi încercarea de a defini ” propoziția adevărată a unui limbaj ” cu un meta-limbaj, apoi având nevoie de un alt meta-limbaj pentru asta, unul …
• Problema este că ceea ce dorește utilizatorul ” ” nu este de obicei exprimat într-un limba! În general, nu există un răspuns formal la întrebarea: ” această specificație formală corespunde ideii mele informale? „. ‘ este posibil să testați o specificație formală și să demonstrați că are anumite proprietăți matematice, dar în cele din urmă trebuie să raportați matematica la lumea reală, care este un proces non-formal.
• Da, desigur – întotdeauna mi-am dat seama că metodele formale ar putea începe doar dintr-un punct bine definit.Dacă specificația respectivă este conformă sau nu cu nevoile conștiente / inconștiente / nedescoperite ale utilizatorilor din viața reală este o altă problemă, care nu poate fi abordată prin metode formale (dar cu siguranță o problemă pentru ingineri).
• O teoremă este, prin definiție, o propunere dovedită. Deci, probabil că nu vrei să ” să demonstrezi teorema „.
• @nbro Wikipedia pare să fie de acord cu tine. Cu toate acestea, Mathworld definește o teoremă ca fiind o propoziție care ” poate fi demonstrată a fi adevărată prin operații matematice acceptate „. În acest caz, oferirea de dovezi ale teoremelor nu este doar posibilă, ci este necesară pentru a justifica numirea lor așa! 🙂 (aceasta este o contracombinare, desigur)

Aș dori să menționez trei aplicații remarcabile de metode formale / instrumente de verificare formală în industrie sau sisteme reale ne-banale. Rețineți că am puțină experiență pe acest subiect și le învăț numai din citirea lucrărilor.

1. Instrumentul open-source Java Pathfinder (JPF pe scurt) lansat de NASA în 2005 este un sistem de verificare a programelor executabile Java bytecode (vezi Java Pathfinder @ wiki ). A fost folosit pentru a detecta neconcordanțe în software-ul executiv pentru K9 Rover la NASA Ames.

2. Acest referat: Utilizarea verificării modelului pentru a găsi erori grave ale sistemului de fișiere @ OSDI „04 arată cum să utilizați verificarea modelului pentru a găsi erori grave în sistemele de fișiere. Un sistem numit FiSC este aplicat la trei sisteme de fișiere foarte utilizate, foarte testate: ext3, JFS și ReiserFS și se găsesc 32 de erori grave. A câștigat Premiul pentru cea mai bună hârtie.

3. Acest referat: Cum Amazon Web Services folosește metodele formale @ CACM „15 descrie modul în care AWS aplică metodele formale produsele sale precum S3, DynamoDB, EBS și Managerul de blocare distribuită internă. Se concentrează pe instrumentul TLA + al lui Lamport. Apropo, Lamport și-a folosit în mod intens propria cutie de instrumente TLA. Deseori face o verificare formală (destul de completă) în TLA a algoritmilor / teoremelor propuse de el însuși (precum și de coautori) în anexele la lucrări.

Verificarea formală este acum posibilă pentru programele scrise cu un subset de C ++ conceput pentru sisteme integrate de siguranță. Consultați http://eschertech.com/papers/CanCPlusPlusBeMadeAsSafeAsSpark.ppt pentru o scurtă prezentare și http://eschertech.com/papers/CanCPlusPlusBeMadeAsSafeAsSpark.pdf pentru lucrarea completă.

Comentarii

• Vă mulțumim pentru linkuri. Cel puțin o scurtă prezentare generală a conținutului lor ar fi utilă, pentru a vă proteja împotriva puterii link-urilor, mai ales că linkurile dvs. sunt către un site web corporativ: acestea tind să fie reorganizate periodic, eliminând toate linkurile către site.

Un formal specificarea unui program este (mai mult sau mai puțin) un program scris într-un alt limbaj de programare. Ca urmare, specificația va include cu siguranță propriile bug-uri.

Avantajul verificării formale este că, întrucât programul și specificația sunt două implementări separate, bug-urile lor vor fi diferite. Dar nu întotdeauna: o sursă obișnuită de erori, cazuri trecute cu vederea, se va potrivi adesea. Astfel, verificarea formală nu este un panaceu: poate lipsi totuși un număr nesemnificativ de bug-uri.

Un dezavantaj al verificării formale este că poate impune ceva de genul dublului costului de implementare, probabil mai mult (aveți nevoie de un specialist în specificații formale și trebuie să utilizați instrumentele mai mult sau mai puțin experimentale care vin cu acesta; care nu vor fi ieftine).

Aș presupune că ar trebui să configurați cazuri de testare și schele pentru a le executa automat ar fi o utilizare mai bună a timpului dvs.

Comentarii

• Avantajul al verificării formale este că … Un al doilea dezavantaj al verificării formale este că … Acest lucru este confuz.
• Cred că nepotrivirea dintre specificație și sarcina informală este o problemă de analiză a cerințelor software, nu o problemă de programare.

Puneți câteva întrebări diferite. Sunt de acord că se pare că metodele de verificare formală pentru aplicațiile industriale / comerciale nu sunt atât de frecvente. ar trebui să ne dăm seama totuși că o mulțime de principii de „verificare formală” sunt încorporate în compilatoare pentru a determina corectitudinea programului! deci, într-un fel, dacă utilizați un compilator modern, utilizați o mare parte din stadiul tehnicii în verificarea formală.

Spuneți că „m-am săturat de testare”, dar verificarea formală nu este într-adevăr un substitut pentru testare. într-un fel este o variație la testare.

Menționați Java.există multe metode avansate de verificare formală încorporate într-un program de verificare Java numit FindBugs care într-adevăr pot fi rulate pe baze de cod mari. Rețineți că va apărea atât „fals pozitiv, cât și fals negativ”, iar rezultatele trebuie revizuite / analizate de un dezvoltator uman. Dar rețineți, chiar dacă nu apare defecte funcționale reale, în general apare „antipatterns” care oricum ar trebui evitate în cod.

Nu faceți mai multe mențiuni despre aplicația dvs. în afară de „industrială”. . Verificarea formală în practică tinde să depindă de aplicația particulară.

Tehnicile de verificare formală par a fi utilizate pe scară largă în EE pentru a dovedi corectitudinea circuitului, de ex. în proiectarea microprocesorului.

Iată un exemplu de sondaj al instrumentelor de verificare formală în câmpul EE de către Lars Philipson .

Comentarii

• Este ‘ înșelător să spunem că ” a o mulțime de principii de ” verificare formală ” sunt încorporate în compilatoare pentru a determina corectitudinea programului „. La ce vă referiți este verificarea statică de tip pe care o fac unele compilatoare, dar proprietățile verificate în acest fel sunt destul de simple, de ex. evitând adăugarea unui număr și a unui șir. Acest lucru este util, dar este departe de ceea ce este de obicei înțeles prin ” verificare formală „.
• consultați în mod specific verificarea tipului static, deși acesta este un exemplu simplu / obișnuit. tehnicile de optimizare a compilatorului imho, care sunt răspândite și avansate, sunt aproximativ similare cu principiile de verificare formală, deoarece implică tehnici avansate pentru a determina / arăta echivalența variantelor de program optimizate. deci se pare că este important să evitați ” poștele în mișcare ” aici și să nu presupuneți acest lucru doar pentru că un compilator o face sau este construită în compilator, verificarea nu este formală.
• a fost de acord că acest lucru nu este o înțelegere comună. tehnicile de optimizare creează aproximativ un model de comportament al programului, de exemplu, al unei bucle sau subrutine, și optimizează acel model și apoi generează un cod nou, care este probabil echivalent. astfel încât unele dintre aceste optimizări sunt destul de sofisticate în rearanjarea codului & pentru mine, ele folosesc principiile de verificare formală. se pare că există multe alte exemple de metode de verificare formală în compilator … întrebarea inițială punea multe întrebări diferite, așa cum mulți au observat, nu încerc să răspund la toate întrebările conținute în acesta.
• de către felul în care par să existe unele principii de verificare formale utilizate și în JRE, motorul de rulare Java, de exemplu optimizarea dinamică, etc …
• adică ” vis de verificare formală ” menționată de filmus mai sus, imho o abstractizare himerică, iar industria pragmatică / utilitară / realistă o recunoaște în mare măsură ca atare. bazele de cod mari se știu de zeci de ani că au inerent $ x $ bug-uri / defecte pe $ y $ K-linii de cod și acest lucru niciodată nu se va schimba indiferent de modul în care teoria / tehnologia avansează, este un fapt de natura umană . și, de fapt, teoremele matematice create de om au aceleași proprietăți, deși acest lucru nu este apreciat pe scară largă!

Poate că un model de verificare poate fi util.

http://alloytools.org/documentation.html Alloy este un model de verificare .

O prezentare frumoasă care explică conceptul de verificare a modelului folosind Alloy: https://www.youtube.com/watch?v=FvNRlE4E9QQ

În aceeași familie de instrumente vine „testarea bazată pe proprietăți”, toți încearcă să găsească un contra-exemplu pentru modelul de specificație dat al software-ului dvs.