Formele programmaverificatie in de praktijk

Ik zal proberen een beknopt antwoord te geven op enkele van uw vragen.Houd er rekening mee dat dit strikt genomen niet mijn onderzoeksgebied is, dus sommige van mijn gegevens kunnen verouderd / onjuist zijn.

1. Er zijn veel tools die specifiek zijn ontworpen om eigenschappen formeel te bewijzen van Java en C ++.

   Ik moet hier echter een kleine uitweiding maken: wat betekent het om de juistheid van een programma te bewijzen? De Java-typecontrole bewijst een formele eigenschap van een Java-programma, namelijk dat bepaalde fouten, zoals het toevoegen van een float en een int, nooit kunnen optreden! Ik stel me voor dat je geïnteresseerd bent in veel sterkere eigenschappen, namelijk dat je programma nooit in een ongewenste toestand kan komen, of dat de uitvoer van een bepaalde functie voldoet aan een bepaalde wiskundige specificatie. Kortom, er is een breed verloop van wat “bewijzen dat een programma correct is” kan betekenen, van eenvoudige beveiligingseigenschappen tot een volledig bewijs dat het programma voldoet aan een gedetailleerde specificatie.

   Nu ga ik ervan uit dat je bent geïnteresseerd in het bewijzen van sterke eigenschappen van je programmas. Als je geïnteresseerd bent in beveiligingseigenschappen (je programma kan niet een bepaalde staat bereiken), dan lijkt het over het algemeen de beste aanpak modelcontrole . Als u echter het gedrag van een Java-programma volledig wilt specificeren, kunt u het beste een specificatietaal voor die taal gebruiken, bijvoorbeeld JML . Er zijn zulke talen om het gedrag van C-programmas te specificeren, bijvoorbeeld ACSL , maar ik weet niets van C ++.

2. Als je eenmaal je specificaties hebt, moet je bewijzen dat het programma aan die specificatie voldoet.

   Hiervoor heb je een tool nodig die een formeel begrip van beide uw specificatie en de operationele semantiek van uw taal (Java of C ++) om de toereikendheidstheorema uit te drukken, namelijk dat de uitvoering van het programma respecteert de specificatie.

   Deze tool zou je ook in staat moeten stellen om het bewijs van die stelling te formuleren of te genereren. Nu zijn beide taken (specificeren en bewijzen) vrij moeilijk, dus worden ze vaak in tweeën gescheiden:

   • Een tool die de code en de specificatie parseert en de toereikendheidstheorema genereert. Zoals Frank al zei, Krakatoa is een voorbeeld van zon tool.

   • Een tool die de stelling bewijst ( s), automatisch of interactief. Coq werkt op deze manier samen met Krakatoa, en er zijn enkele krachtige geautomatiseerde tools zoals Z3 die ook kunnen worden gebruikt.

   Een (klein) punt: er zijn een aantal stellingen die veel te moeilijk zijn om bewezen te worden met geautomatiseerde methoden, en het is bekend dat automatische bewijsmakers van stellingen af en toe deugdelijkheidsfoutjes hebben die ze minder betrouwbaar maken. Dit is een gebied waar Coq uitblinkt in vergelijking (maar het is niet automatisch!).

3. Als je Ocaml-code wilt genereren, schrijf dan zeker eerst in Coq (Gallina), extraheer vervolgens de code. Coq is echter verschrikkelijk in het genereren van C ++ of Java, als het zelfs maar mogelijk is.

4. Kunnen de bovenstaande tools omgaan met threading- en prestatieproblemen? Waarschijnlijk niet, problemen met de prestaties en het inrijgen kunnen het beste worden aangepakt door speciaal ontworpen gereedschappen, aangezien het bijzonder moeilijke problemen zijn. Ik weet niet zeker of ik hier tools heb om aan te bevelen, hoewel het PolyNI -project van Martin Hofmann interessant lijkt.

Concluderend: formele verificatie van “echte” Java- en C ++ -programmas is een groot en goed ontwikkeld veld, en Coq is geschikt voor delen van die taak. U kunt bijvoorbeeld hier een overzicht op hoog niveau vinden.

Opmerkingen

• Bedankt voor dit bericht en de referenties die je hebt toegevoegd. IMHO, het doel voor software-ingenieurs is om snel systemen te kunnen vrijgeven die 1) altijd de juiste resultaten opleveren, 2) nooit falen. Ik zou hier een regressieprobleem kunnen zien, waarbij je misschien wilt bewijzen dat de specificatie zelf ” bugvrij is ” 🙂 soort van zoals het proberen ” ware propositie van een taal ” te definiëren met een metataal, en daarvoor een andere metataal nodig te hebben, dan nog een one …
• Het probleem is dat wat de gebruiker ” wil ” meestal niet wordt uitgedrukt in een formele taal! Er is doorgaans geen formeel antwoord op de vraag: ” komt deze formele specificatie overeen met mijn informele idee? “. Het ‘ is mogelijk om een formele specificatie te testen en te bewijzen dat deze bepaalde wiskundige eigenschappen heeft, maar uiteindelijk moet je de wiskunde relateren aan de echte wereld, dat is een niet-formeel proces.
• Ja natuurlijk – ik realiseerde me altijd dat de formele methoden alleen konden beginnen vanaf een welomschreven punt.Of die specificatie al dan niet overeenstemt met de bewuste / onbewuste / onontdekte behoeften van gebruikers in het echte leven, is een ander probleem dat niet kan worden aangepakt met formele methoden (maar zeker een probleem voor ingenieurs).
• Een stelling is per definitie een bewezen voorstel. Het is dus waarschijnlijk niet uw bedoeling om ” de stelling ” te bewijzen.
• @nbro Wikipedia lijkt het daarmee eens te zijn met jou. Mathworld definieert een stelling echter als een propositie waarvan ” kan worden aangetoond dat deze waar is door geaccepteerde wiskundige bewerkingen “. In dit geval is het leveren van bewijzen van stellingen niet alleen mogelijk, maar ook noodzakelijk om ze zo te noemen! 🙂 (dit is natuurlijk een tegenvraag)

Ik wil drie opmerkelijke toepassingen noemen van formele methoden / formele verificatie-instrumenten in de industrie of niet-triviale echte systemen. Merk op dat ik weinig ervaring heb met dit onderwerp en ik leer ze alleen door het lezen van papers.

1. De open-source tool Java Pathfinder (afgekort JPF) uitgebracht door NASA in 2005 is een systeem om uitvoerbare Java-bytecode-programmas te verifiëren (zie Java Pathfinder @ wiki ). Het is gebruikt om inconsistenties op te sporen in de uitvoerende software voor de K9 Rover bij NASA Ames.

2. Dit artikel: Modelcontrole gebruiken om ernstige bestandssysteemfouten op te sporen @ OSDI “04 laat zien hoe u modelcontrole om ernstige fouten in bestandssystemen te vinden. Een systeem genaamd FiSC wordt toegepast op drie veelgebruikte, zwaar geteste bestandssystemen: ext3, JFS en ReiserFS, en er zijn 32 ernstige bugs gevonden. Het heeft de Best Paper Award gewonnen.

3. Dit artikel: Hoe Amazon Web Services formele methoden gebruikt @ CACM “15 beschrijft hoe AWS formele methoden toepast op zijn producten zoals S3, DynamoDB, EBS en Internal distributed lock manager. Het richt zich op Lamport “s TLA + tool. Lamport heeft trouwens intensief gebruik gemaakt van zijn eigen TLA toolbox. Hij geeft vaak een (vrij volledige) formele verificatie in TLA van de algoritmen / stellingen die door hemzelf (en mede-auteurs) zijn voorgesteld in bijlagen bij de artikelen.

Formele verificatie is nu mogelijk voor programmas die zijn geschreven met een subset van C ++ en ontworpen zijn voor veiligheidskritieke embedded systemen. Zie http://eschertech.com/papers/CanCPlusPlusBeMadeAsSafeAsSpark.ppt voor een korte presentatie en http://eschertech.com/papers/CanCPlusPlusBeMadeAsSafeAsSpark.pdf voor het volledige artikel.

Opmerkingen

• Bedankt voor de links. Een kort overzicht van hun inhoud zou in ieder geval nuttig zijn, ter bescherming tegen link-rot, vooral omdat uw links naar een bedrijfswebsite zijn: die hebben de neiging om periodiek te worden gereorganiseerd, waardoor alle links naar de site worden vernietigd.

Een formele specificatie van een programma is (min of meer) een programma geschreven in een andere programmeertaal. Als resultaat zal de specificatie zeker zijn eigen bugs bevatten.

Het voordeel van formele verificatie is dat, aangezien het programma en de specificatie twee afzonderlijke implementaties zijn, hun bugs verschillend zullen zijn. Maar niet altijd: een veelvoorkomende bron van bugs, over het hoofd geziene gevallen, komt vaak overeen. Formele verificatie is dus geen wondermiddel: het kan nog steeds een niet-triviaal aantal bugs missen.

Een nadeel van formele verificatie is dat het zoiets als twee keer de implementatiekost kan opleggen, waarschijnlijk meer (je hebt een specialist in formele specificaties, en je moet de min of meer experimentele tools gebruiken die erbij horen; dat is niet goedkoop).

Ik denk dat het opzetten van testcases en steigers om ze uit te voeren automatisch een betere besteding van uw tijd zijn.

Opmerkingen

• Het voordeel van formele verificatie is dat … . Een tweede nadeel van formele verificatie is dat … Dit is verwarrend.
• Ik denk dat de discrepantie tussen specificatie en informele taak een kwestie is van de analyse van softwarevereisten en niet van een programmeerprobleem.

Je stelt een paar verschillende vragen. Ik ben het ermee eens dat het lijkt alsof formele verificatiemethoden voor industriële / commerciële toepassingen niet zo gebruikelijk zijn. men moet zich echter realiseren dat veel “formele verificatie” -principes in compilers zijn ingebouwd om de correctheid van het programma te bepalen! dus als je een moderne compiler gebruikt, gebruik je in zekere zin veel van de allernieuwste in formele verificatie.

Je zegt ik ben het testen beu, maar formele verificatie is niet echt een vervanging voor testen. in zekere zin is het een variatie op testen.

U noemt Java.er zijn veel geavanceerde formele verificatiemethoden ingebouwd in een Java-verificatieprogramma genaamd FindBugs die inderdaad over grote codebases kunnen worden uitgevoerd. Merk op dat het zowel “valse positieven als valse negatieven” zal opleveren en dat de resultaten moeten worden beoordeeld / geanalyseerd door een menselijke ontwikkelaar. Maar merk op dat zelfs als het geen echte functionele defecten aan het licht brengt, het in het algemeen wel “antipatronen” opduikt die hoe dan ook in de code moeten worden vermeden.

U maakt niet meer melding van uw specifieke toepassing anders dan “industrieel” . Formele verificatie in de praktijk is meestal afhankelijk van de specifieke toepassing.

Formele verificatietechnieken lijken op grote schaal te worden gebruikt in EE om circuitcorrectheid te bewijzen, bijv. in microprocessorontwerp.

Hier is een voorbeeld van een overzicht van formele verificatietools in het EE-veld door Lars Philipson .

Reacties

• Het ‘ is misleidend om te zeggen dat ” a veel ” formele verificatie ” principes zijn ingebouwd in compilers om de correctheid van het programma te bepalen “. Waar u naar verwijst, is statische typecontrole die sommige compilers doen, maar de op die manier geverifieerde eigenschappen zijn vrij eenvoudig, bijv. vermijd het toevoegen van een nummer en een string. Dit is nuttig, maar staat ver af van wat gewoonlijk wordt onderschat door ” formele verificatie “.
• niet verwijzen specifiek naar statische typecontrole, hoewel dat een eenvoudig / algemeen voorbeeld is. De imho-compileroptimalisatietechnieken, die wijdverbreid en geavanceerd zijn, lijken ruwweg op formele verificatieprincipes, omdat ze geavanceerde technieken omvatten om de gelijkwaardigheid van geoptimaliseerde programmavarianten te bepalen / aantonen. het lijkt dus belangrijk om het probleem ” bewegende doelpalen ” hier te vermijden en niet aan te nemen dat alleen omdat een compiler het doet of het is gebouwd in de compiler, het is geen formele verificatie.
• was het erover eens dat dit geen algemeen begrip is. de optimalisatietechnieken zijn grofweg het creëren van een model van programmagedrag, bijvoorbeeld van een lus of subroutine, en het optimaliseren van dat model, en vervolgens het genereren van nieuwe code die aantoonbaar equivalent is. dus sommige van deze optimalisaties zijn behoorlijk geavanceerd in het herschikken van code & voor mij maken ze gebruik van formele verificatieprincipes. er lijken veel andere voorbeelden te zijn van formele verificatiemethoden in de compiler … de oorspronkelijke vraag stelde veel verschillende vragen zoals velen hebben opgemerkt, ik probeer zeker niet alle vragen te beantwoorden die erin staan.
• door de er lijken enkele formele verificatieprincipes te zijn die ook worden gebruikt in de JRE, java runtime-engine, bijv. dynamische optimalisatie, enz …
• dat is ” de droom van formele verificatie ” waarnaar wordt verwezen door filmus hierboven, imho een chimere abstractie, en de pragmatische / utilitaire / realistische industrie herkent het grotendeels als zodanig. Van grote codebases is al decennia bekend dat ze inherent $ x $ bugs / defecten per $ y $ K-regels code bevatten en dit zal nooit veranderen, ongeacht hoe de theorie / technologie zich ontwikkelt, het is een feit van menselijke natuur. en in feite hebben door mensen gemaakte wiskundige stellingen dezelfde eigenschappen, hoewel dit niet algemeen wordt gewaardeerd!

Misschien kan een modelcontrole nuttig zijn.

http://alloytools.org/documentation.html Legering is een modelcontrole .

Een mooie presentatie waarin het concept van modelcontrole met legering wordt uitgelegd: https://www.youtube.com/watch?v=FvNRlE4E9QQ

In dezelfde familie van tools komt “property-based testing”, ze proberen allemaal een tegenvoorbeeld te vinden voor het gegeven specificatiemodel van je software.