Formell programverifisering i praksis

Jeg vil prøve å gi et kortfattet svar på noen av spørsmålene dine.Vær oppmerksom på at dette ikke er strengt mitt forskningsfelt, så noe av informasjonen min kan være utdatert / feil.

1. Det er mange verktøy som er spesielt utviklet for å formelt bevise egenskaper av Java og C ++.

   Men jeg må gjøre en liten avvikelse her: hva betyr det å bevise riktigheten av et program? Java-typekontrolløren viser en formell egenskap til et Java-program, nemlig at visse feil, som å legge til en float og en int, aldri kan skje! Jeg forestiller meg at du er interessert i mye sterkere egenskaper, nemlig at programmet ditt aldri kan komme i en uønsket tilstand, eller at utdataene til en bestemt funksjon samsvarer med en viss matematisk spesifikasjon. Kort fortalt er det en bred gradient av hva «å bevise et program riktig» kan bety, fra enkle sikkerhetsegenskaper til et fullstendig bevis på at programmet oppfyller en detaljert spesifikasjon.

   Nå skal jeg anta at du er interessert i å bevise sterke egenskaper om programmene dine. Hvis du er interessert i sikkerhetsegenskaper (programmet ditt kan ikke nå en viss tilstand), ser det generelt ut til at den beste tilnærmingen er modellkontroll . Hvis du imidlertid vil spesifisere oppførselen til et Java-program, er det best å bruke et spesifikasjonsspråk for det språket, for eksempel JML . Det er slike språk for å spesifisere oppførselen til C-programmer, for eksempel ACSL , men jeg vet ikke om C ++.

2. Når du har spesifikasjonene dine, må du bevise at programmet samsvarer med den spesifikasjonen.

   For dette trenger du et verktøy som har en formell forståelse av begge deler spesifikasjonen din og den operative semantikken til språket ditt (Java eller C ++) for å uttrykke tilstrekkelig teorem , nemlig at utførelsen av programmet respekterer spesifikasjonen.

   Dette verktøyet skal også tillate deg å formulere eller generere bevis for den teoremet. Nå er begge disse oppgavene (å spesifisere og bevise) ganske vanskelige, så de skilles ofte i to:

   • Ett verktøy som analyserer koden, spesifikasjonen og genererer tilstrekkelige teorem. Som Frank nevnte er Krakatoa et eksempel på et slikt verktøy.

   • Ett verktøy som beviser setningen ( s), automatisk eller interaktivt. Coq samhandler med Krakatoa på denne måten, og det er noen kraftige automatiserte verktøy som Z3 som også kan brukes.

   Ett (mindre) poeng: det er noen teoremer som det er altfor vanskelig å bevise med automatiserte metoder, og det er kjent at automatiske teoremeldere av og til har lydfeil som gjør dem mindre pålitelige. Dette er et område der Coq skinner i sammenligning (men det er ikke automatisk!).

3. Hvis du vil generere Ocaml-kode, så skriv i Coq (Gallina) først, trekk deretter ut koden. Coq er imidlertid forferdelig til å generere C ++ eller Java, hvis det til og med er mulig.

4. Kan de ovennevnte verktøyene håndtere tråd- og ytelsesproblemer? Sannsynligvis ikke, ytelses- og trådproblemer håndteres best av spesialdesignede verktøy, da de er spesielt vanskelige problemer. Jeg er ikke sikker på at jeg har noen verktøy å anbefale her, selv om Martin Hofmann s PolyNI -prosjekt virker interessant.

ol Avslutningsvis: formell verifisering av «virkelige verden» Java- og C ++ – programmer er et stort og godt utviklet felt, og Coq er egnet for deler av den oppgaven. Du kan for eksempel finne en oversikt på høyt nivå her .

Kommentarer

• Takk for dette innlegget og referansene du la til. IMHO, målet for programvareingeniører er å være i stand til raskt å frigjøre systemer som 1) alltid vil gi riktige resultater, 2) aldri mislykkes. Jeg kunne se et regresjonsproblem her, der du kanskje vil bevise at spesifikasjonen i seg selv er » feilfri » 🙂 slags som å prøve å definere » ekte proposisjon av et språk » med et metaspråk, og deretter trenge et nytt metaspråk for det, så et annet en …
• Problemet er at det brukeren » ønsker » vanligvis ikke uttrykkes i en formell Språk! Det er generelt ikke noe formelt svar på spørsmålet: » samsvarer denne formelle spesifikasjonen med min uformelle idé? «. Det er ‘ mulig å teste en formell spesifikasjon, og bevise at den har visse matematiske egenskaper, men til slutt må du knytte matematikken til den virkelige verden, som er en ikke-formell prosess.
• Ja selvfølgelig – jeg har alltid innsett at de formelle metodene bare kunne starte fra et veldefinert punkt.Hvis spesifikasjonen samsvarer med eller ikke de bevisste / ubevisste / uoppdagede behovene til brukere fra virkelige liv, er et annet problem, som ikke kan adresseres med formelle metoder (men absolutt et problem for ingeniører).
• En teorem er per definisjon en bevist proposisjon. Så du mener sannsynligvis ikke å » bevise setningen «.
• @nbro Wikipedia ser ut til å være enig med deg. Mathworld definerer imidlertid en teorem som en proposisjon som » kan demonstreres for å være sant ved aksepterte matematiske operasjoner «. I dette tilfellet er det ikke bare mulig å gi bevis på setninger, men nødvendig for å rettferdiggjøre å kalle dem det! 🙂 (dette er selvfølgelig en motkonkurranse)

Jeg vil nevne tre bemerkelsesverdige applikasjoner av formelle metoder / formelle verifiseringsverktøy i industrien eller ikke-trivielle reelle systemer. Merk at jeg har liten erfaring med dette emnet, og jeg lærer dem bare av å lese papirer.

1. Open source-verktøyet Java Pathfinder (forkortet JPF) utgitt av NASA i 2005 er et system for å verifisere kjørbare Java bytecode-programmer (se Java Pathfinder @ wiki ). Den har blitt brukt til å oppdage uoverensstemmelser i programvaren for K9 Rover på NASA Ames.

2. Dette papiret: Bruke modellkontroll for å finne alvorlige filsystemfeil @ OSDI «04 viser hvordan du bruker modellkontroll for å finne alvorlige feil i filsystemer. Et system kalt FiSC brukes på tre mye brukte, høyt testede filsystemer: ext3, JFS og ReiserFS, og 32 alvorlige feil blir funnet. Det vant Best Paper Award.

3. Denne artikkelen: Hvordan Amazon Web Services bruker formelle metoder @ CACM «15 beskriver hvordan AWS bruker formelle metoder på sine produkter som S3, DynamoDB, EBS og intern distribuert låsebehandler. Den fokuserer på Lamports TLA + -verktøy. Forresten har Lamport intensivt brukt sin egen TLA-verktøykasse. Han gir ofte en (ganske fullstendig) formell verifisering i TLA av algoritmene / teoremene som er foreslått av ham selv (samt medforfattere) i vedlegg til papirene.

Formell bekreftelse er nå mulig for programmer skrevet en delmengde av C ++ designet for sikkerhetskritiske innebygde systemer. Se http://eschertech.com/papers/CanCPlusPlusBeMadeAsSafeAsSpark.ppt for en kort presentasjon, og http://eschertech.com/papers/CanCPlusPlusBeMadeAsSafeAsSpark.pdf for hele papiret.

Kommentarer

• Takk for lenkene. I det minste vil en kort oversikt over innholdet være nyttig, for å beskytte mot link-rot, spesielt siden linkene dine er til et bedriftsnettsted: de har en tendens til å bli omorganisert med jevne mellomrom, og dreper alle lenker til nettstedet.

En formell spesifikasjon av et program er (mer eller mindre) et program skrevet på et annet programmeringsspråk. Som et resultat vil spesifikasjonen absolutt inkludere sine egne bugs.

Fordelen med formell verifisering er at ettersom programmet og spesifikasjonen er to separate implementeringer, vil deres bugs være forskjellige. Men ikke alltid: en vanlig kilde til feil, oversett tilfeller, vil ofte matche. Dermed er ikke formell bekreftelse et universalmiddel: den kan fortsatt savne et ikke-trivielt antall feil.

En ulempe med formell bekreftelse er at den kan påføre noe som dobbelt så mye implementeringskostnad, sannsynligvis mer (du trenger en spesialist i formell spesifikasjon, og du må bruke de mer eller mindre eksperimentelle verktøyene som følger med det, som ikke blir billig).

Jeg antar å sette opp testsaker og stillas for å kjøre dem automatisk ville være en bedre bruk av tiden din.

Kommentarer

• fordelen av formell bekreftelse er at … En annen ulempe av formell bekreftelse er at … Dette er forvirrende.
• Jeg tror at uoverensstemmelse mellom spesifikasjon og uformell oppgave er et problem med programvarekravsanalyse, ikke et programmeringsproblem.

Du stiller noen få forskjellige spørsmål. Jeg er enig i at det ser ut til at formelle verifikasjonsmetoder for industrielle / kommersielle applikasjoner ikke er så vanlige. man må imidlertid innse at mange «formelle verifikasjons» -prinsipper er innebygd i kompilatorer for å bestemme programkorrektheten! så på en måte, hvis du bruker en moderne kompilator, bruker du mye av det nyeste innen formell verifisering.

Du sier «Jeg er lei av å teste» men formell bekreftelse er egentlig ikke en erstatning for testing. på en måte er det en variant på testing.

Du nevner Java.det er mange avanserte formelle verifiseringsmetoder innebygd i et java-verifikasjonsprogram kalt FindBugs som faktisk kan kjøres over store kodebaser. Legg merke til at det vil dukke opp både «falske positive og falske negative», og resultatene må gjennomgås / analyseres av en menneskelig utvikler. Men vær oppmerksom på at selv om det ikke viser reelle funksjonsfeil, viser det generelt «antipatterns» som uansett bør unngås i koden.

Du nevner ikke mer din spesifikke applikasjon enn «industriell» . Formell verifisering har i praksis en tendens til å avhenge av den spesifikke applikasjonen.

Formelle verifiseringsteknikker ser ut til å være mye brukt i EE for å bevise kretskorrekthet, f.eks. i mikroprosessordesign.

Her er et eksempel på en kartlegging av formelle verifiseringsverktøy i EE-feltet av Lars Philipson .

Kommentarer

• Det ‘ er villedende å si at » en mye » formell bekreftelse » prinsipper er innebygd i kompilatorer for å bestemme programkorrekthet «. Det du refererer til er statisk typekontroll som noen kompilatorer gjør, men egenskapene som er verifisert på den måten er ganske enkle, f.eks. unngå å legge til et tall og en streng. Dette er nyttig, men langt fra det som vanligvis understodd av » formell bekreftelse «.
• gjorde ikke referer til statisk typekontroll spesielt, selv om det er et enkelt / vanlig eksempel. imho kompilatoroptimaliseringsteknikker, som er utbredt og avansert, ligner omtrent formelle verifikasjonsprinsipper, fordi de involverer avanserte teknikker for å bestemme / vise ekvivalens av optimaliserte programvarianter. så det ser ut til at det er viktig å unngå » bevegelige målstolper » problemet her og ikke anta at bare fordi en kompilator gjør det eller er bygget inn i kompilatoren, er det ikke formell bekreftelse.
• enige om at dette ikke er en vanlig forståelse. Optimaliseringsteknikkene skaper omtrent en modell for programatferd, f.eks. av en loop eller subrutine, og optimaliserer den modellen, og genererer deretter ny kode som er beviselig ekvivalent. så noen av disse optimaliseringene er ganske sofistikerte når det gjelder å omorganisere kode & for meg, de bruker formelle bekreftelsesprinsipper. det ser ut til å være mange andre eksempler på formelle verifiseringsmetoder i kompilatoren … det opprinnelige spørsmålet stilte mange forskjellige spørsmål som mange har bemerket, og jeg prøver ikke å svare på alle spørsmålene i den.
• av måten det ser ut til å være noen formelle bekreftelsesprinsipper også brukt i JRE, java runtime engine, f.eks. dynamisk optimalisering, etc …
• det vil si » drømmer om formell verifisering » referert til av filmus ovenfor, imho en kimær abstraksjon, og pragmatisk / utilitaristisk / realistisk industri anerkjenner den i stor grad som sådan. store kodebaser har vært kjent i flere tiår for iboende å ha $ x $ bugs / defekter per $ y $ K-linjer med kode, og dette vil aldri endre seg uansett hvordan teori / teknologi utvikler seg, det er et faktum menneskelig natur. og faktisk menneskeskapte matematiske teoremer har de samme egenskapene, selv om dette ikke blir satt stor pris på!

En modellkontroll kan kanskje være nyttig.

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

En fin presentasjon som forklarer begrepet modellkontroll ved bruk av legering: https://www.youtube.com/watch?v=FvNRlE4E9QQ

I samme familie av verktøy kommer «eiendomsbasert testing», de prøver alle å finne et moteksempel for den gitte spesifikasjonsmodellen for programvaren din.