Formel programverifikation i praksis

Jeg vil prøve at give et kortfattet svar på nogle af dine spørgsmål.Vær opmærksom på, at dette ikke strengt er mit forskningsfelt, så nogle af mine oplysninger kan være forældede / forkerte.

1. Der er mange værktøjer, der er specielt designet til formelt at bevise egenskaber af Java og C ++.

   Men jeg er nødt til at gøre en lille afvigelse her: hvad betyder det at bevise rigtigheden af et program? Java-typekontrollen viser en formel egenskab ved et Java-program, nemlig at visse fejl, som tilføjelse af en float og en int, aldrig kan forekomme! Jeg forestiller mig, at du er interesseret i meget stærkere egenskaber, nemlig at dit program aldrig kan gå i en uønsket tilstand, eller at output fra en bestemt funktion er i overensstemmelse med en bestemt matematisk specifikation. Kort sagt er der en bred gradient af, hvad “at bevise et program korrekt” kan betyde, fra enkle sikkerhedsegenskaber til et fuldt bevis for, at programmet opfylder en detaljeret specifikation.

   Nu vil jeg antage, at du er interesseret i at bevise stærke egenskaber om dine programmer. Hvis du er interesseret i sikkerhedsegenskaber (dit program kan ikke nå en bestemt tilstand), ser det generelt ud til, at den bedste tilgang er modelkontrol . Men hvis du fuldt ud ønsker at specificere et Java-programs opførsel, er det bedst at bruge et specifikationssprog til dette sprog, f.eks. JML . Der er sådanne sprog til at specificere C-programmernes opførsel, for eksempel ACSL , men jeg ved ikke om C ++.

2. Når du har dine specifikationer, skal du bevise, at programmet overholder den specifikation.

   Til dette har du brug for et værktøj, der har en formel forståelse af begge dele din specifikation og den operationelle semantik i dit sprog (Java eller C ++) for at udtrykke tilstrækkelighedssætningen , nemlig at udførelsen af programmet respekterer specifikationen.

   Dette værktøj skal også give dig mulighed for at formulere eller generere bevis for denne sætning. Nu er begge disse opgaver (at specificere og bevise) ret vanskelige, så de adskilles ofte i to:

   • Et værktøj, der analyserer koden, specifikationen og genererer tilstrækkelighedssætningen. Som Frank nævnte, er Krakatoa et eksempel på et sådant værktøj.

   • Et værktøj, der beviser sætningen ( s) automatisk eller interaktivt. Coq interagerer med Krakatoa på denne måde, og der er nogle kraftfulde automatiserede værktøjer som Z3 , som også kan bruges.

   Et (mindre) punkt: der er nogle sætninger, der er alt for vanskelige at blive bevist med automatiserede metoder, og det er kendt, at automatiske sætningsprovers lejlighedsvis har lydstyrkefejl, der gør dem mindre troværdige. Dette er et område, hvor Coq skinner i sammenligning (men det er ikke automatisk!).

3. Hvis du vil generere Ocaml-kode, skal du helt sikkert skrive Coq (Gallina) først, udpak derefter koden. Coq er dog forfærdeligt til at generere C ++ eller Java, hvis det overhovedet er muligt.

4. Kan ovenstående værktøjer håndtere threading og ydeevne problemer? Sandsynligvis ikke, ydeevne og trådningsproblemer håndteres bedst af specifikt designede værktøjer, da de er særligt hårde problemer. Jeg er ikke sikker på, at jeg har nogen værktøjer at anbefale her, selvom Martin Hofmanns projekt PolyNI virker interessant.

Afslutningsvis: formel verifikation af “virkelige verden” Java- og C ++ – programmer er et stort og veludviklet felt, og Coq er velegnet til dele af denne opgave. Du kan f.eks. Finde en oversigt på højt niveau her .

Kommentarer

• Tak for dette indlæg og de referencer, du tilføjede. IMHO, målet for softwareingeniører er at være i stand til hurtigt at frigive systemer, der 1) altid giver korrekte resultater, 2) aldrig fejler. Jeg kunne se et regressionsproblem her, hvor du måske vil bevise, at selve specifikationen er ” bugfri ” 🙂 slags som at prøve at definere ” ægte proposition af et sprog ” med et metasprog og derefter have brug for et andet metasprog til det, så et andet en …
• Problemet er, at hvad brugeren ” ønsker ” normalt ikke udtrykkes i en formel Sprog! Der er generelt intet formelt svar på spørgsmålet: ” Er denne formelle specifikation i overensstemmelse med min uformelle idé? “. Det er ‘ muligt at teste en formel specifikation og bevise, at den har visse matematiske egenskaber, men i sidste ende skal du relatere matematikken til den virkelige verden, hvilket er en ikke-formel proces.
• Ja selvfølgelig – Jeg har altid indset, at de formelle metoder kun kunne starte fra et veldefineret punkt.Hvis denne specifikation er i overensstemmelse med eller ikke til de bevidste / ubevidste / uopdagede behov hos brugere i det virkelige liv, er et andet problem, der ikke kan adresseres med formelle metoder (men bestemt et problem for ingeniører).
• En sætning er pr. Definition en bevist forslag. Så du mener sandsynligvis ikke at ” bevise sætningen “.
• @nbro Wikipedia synes at være enig med dig. Mathworld definerer dog en sætning som en proposition, som ” kan demonstreres som sand ved accepterede matematiske operationer “. I dette tilfælde er det ikke kun muligt at give bevis for sætninger, men det er nødvendigt for at retfærdiggøre at kalde dem det! 🙂 (dette er selvfølgelig en modkæmpelse)

Jeg vil gerne nævne tre bemærkelsesværdige applikationer af formelle metoder / formelle verifikationsværktøjer i industrien eller ikke-trivielle reelle systemer. Bemærk, at jeg har ringe erfaring med dette emne, og at jeg kun lærer dem af læsning af papirer.

1. Open source-værktøjet Java Pathfinder (JPF for kort) udgivet af NASA i 2005 er et system til at verificere eksekverbare Java bytecode-programmer (se Java Pathfinder @ wiki ). Det er blevet brugt til at opdage uoverensstemmelser i den eksekutive software til K9 Rover på NASA Ames.

2. Dette papir: Brug af modelkontrol for at finde alvorlige filsystemfejl @ OSDI “04 viser, hvordan man bruger modelkontrol for at finde alvorlige fejl i filsystemer. Et system kaldet FiSC anvendes til tre meget anvendte, meget testede filsystemer: ext3, JFS og ReiserFS, og der findes 32 alvorlige fejl. Det vandt Best Paper Award.

3. Dette papir: Hvordan Amazon Web Services bruger formelle metoder @ CACM “15 beskriver, hvordan AWS anvender formelle metoder til dets produkter som S3, DynamoDB, EBS og intern distribueret låsemanager. Det fokuserer på Lamports TLA + værktøj. Forresten har Lamport intensivt brugt sin egen TLA-værktøjskasse. Han giver ofte en (ganske komplet) formel verifikation i TLA af algoritmer / sætninger, som han selv har foreslået (samt medforfattere) i bilag til papirerne.

En formel specifikation af et program er (mere eller mindre) et program skrevet på et andet programmeringssprog. Som et resultat vil specifikationen helt sikkert omfatte sine egne bugs.

Fordelen ved formel verifikation er, at da programmet og specifikationen er to separate implementeringer, vil deres bugs være forskellige. Men ikke altid: en almindelig kilde til fejl, oversete tilfælde, vil ofte matche. Formel verifikation er således ikke et universalmiddel: den kan stadig gå glip af et ikke-trivielt antal bugs.

En ulempe ved formel verifikation er, at den kan pålægge noget som dobbelt så meget som implementeringsomkostningerne, sandsynligvis mere (du har brug for en specialist i formel specifikation, og du skal bruge de mere eller mindre eksperimentelle værktøjer, der følger med det, der ikke kommer billigt).

Jeg gætter på at opsætte testcases og stilladser for at køre dem automatisk ville være en bedre udnyttelse af din tid.

Kommentarer

• fordelen af formel verifikation er, at … En anden ulempe af formel verifikation er, at … Dette er forvirrende.
• Jeg tror, at uoverensstemmelse mellem specifikation og uformel opgave er et problem med analyse af softwarekrav, ikke et programmeringsproblem.

Du stiller et par forskellige spørgsmål. Jeg er enig i, at det ser ud til, at formelle verifikationsmetoder til industrielle / kommercielle applikationer ikke er så almindelige. man skal dog indse, at mange “formelle verifikationsprincipper” er indbygget i kompilatorer for at bestemme programkorrekthed! så på en måde, hvis du bruger en moderne kompilator, bruger du meget af det nyeste inden for formel verifikation.

Du siger “Jeg er træt af at teste” men formel verifikation er ikke rigtig en erstatning for testning. på en måde er det en variation på test.

Du nævner Java.der er mange avancerede formelle verifikationsmetoder indbygget i et java-verifikationsprogram kaldet FindBugs , som faktisk kan køres over store kodebaser. Bemærk, at der både “falske positive og falske negativer” vises, og resultaterne skal gennemgås / analyseres af en menneskelig udvikler. Men bemærk, selvom det ikke viser reelle funktionsfejl, viser det generelt “antipatterns”, der alligevel skal undgås i kode.

Du nævner ikke mere din applikation end “industriel” . Formel verifikation i praksis har en tendens til at afhænge af den specifikke anvendelse.

Formelle verifikationsteknikker synes at være vidt anvendte i EE for at bevise kredsløbets korrekthed, f.eks. i mikroprocessordesign.

Her er et eksempel på en oversigt over formelle verifikationsværktøjer i EE-feltet af Lars Philipson .

Kommentarer

• Det ‘ er vildledende at sige, at ” en masse af ” formel verifikation ” principper er indbygget i kompilatorer for at bestemme programkorrekthed “. Det, du refererer til, er statisk typekontrol, som nogle kompilatorer udfører, men de egenskaber, der er verificeret på den måde, er ret enkle, f.eks. undgå at tilføje et tal og en streng. Dette er nyttigt, men langt fra hvad der normalt understoddes af ” formel verifikation “.
• gjorde det ikke henvises specifikt til statisk typekontrol, selvom det er et simpelt / almindeligt eksempel. imho kompilatoroptimeringsteknikker, som er udbredt og avanceret, svarer stort set til formelle verifikationsprincipper, fordi de involverer avancerede teknikker til at bestemme / vise ækvivalens af optimerede programvarianter. så det ser ud til at det er vigtigt at undgå ” bevægelige målposter ” problemet her og ikke antage, at det kun fordi en kompilator gør det eller er bygget ind i kompilatoren er dens ikke formelle verifikation.
• enige om, at dette ikke er en fælles forståelse. optimeringsteknikkerne groft er at skabe en model for programadfærd, f.eks. af en loop eller subrutine, og optimere denne model og derefter generere ny kode, der er beviseligt ækvivalent. så nogle af disse optimeringer er ret sofistikerede ved omarrangering af kode & for mig, de bruger formelle verifikationsprincipper. der synes at være mange andre eksempler på formelle verifikationsmetoder i kompilatoren … det originale spørgsmål stillede mange forskellige spørgsmål, som mange har bemærket, og jeg prøver ikke at besvare alle de spørgsmål, der er indeholdt deri.
• af måde der synes at være nogle formelle verifikationsprincipper, der også bruges i JRE, java runtime-motoren, f.eks. dynamisk optimering osv …
• det vil sige ” drømmer om formel verifikation “, der er omtalt af filmus ovenfor, imho en kimærisk abstraktion, og pragmatisk / utilitaristisk / realistisk industri anerkender stort set den som sådan. store kodebaser har været kendt i årtier til i sagens natur at have $ x $ bugs / defekter pr. $ y $ K-linjer med kode, og dette vil aldrig ændre sig, uanset hvordan teori / teknologi udvikler sig, det er et faktum af menneskelig natur. og faktisk menneskeskabte matematiske sætninger har de samme egenskaber, selvom dette ikke er bredt værdsat!

Måske kan en modelkontrol være nyttig.

http://alloytools.org/documentation.html Legering er en modelkontrol .

En flot præsentation, der forklarer konceptet med modelkontrol ved hjælp af legering: https://www.youtube.com/watch?v=FvNRlE4E9QQ

I den samme familie af værktøjer kommer “ejendomsbaseret test”, de prøver alle at finde et modeksempel til den givne specifikationsmodel for din software.