'Nobelprijs' informatica voor opsporen hard- en softwarefouten

De Turing Award voor 2007 is toegekend aan Edmund M. Clarke, E. Allen Emerson en Joseph Sifakis voor hun onderzoek op het gebied van model checking. Aan de award is prijzengeld van 250.000 dollar verbonden.

De prestigieuze prijs, die officieus te boek staat als de Nobelprijs voor de informatica, is toegekend aan de drie vanwege hun baanbrekend werk op het gebied van opsporingstechnologie voor hard- en softwarefouten. "Zonder de conceptuele doorbraak van deze onderzoekers zouden we nog steeds zitten met chips vol fouten en trage systemen", aldus Stuart Feldman, president van de ACM die de Turing Awards uitreikt. Clark van de Carnegie Mellon-universiteit en zijn voormalige student Emerson van de University of Texas in Austin werkten samen aan het onderzoek, terwijl Sifakis van de universiteit van Grenoble eigen onderzoek deed.

Met model checking worden de mogelijke statussen van een hardware- of software-ontwerp doorlopen om te bepalen of het consistent is met de specificaties van de ontwerper. Clarke en Emerson ontwikkelden de theorie in 1981 aan de universiteit van Harvard. Hun systeem kon bij het niet voldoen aan een specificatie ook de bron van het probleem aangeven.

De eerste implementatie van de theorie volgde in 1982, maar deze kon maar kleine chipontwerpen verifieren. Pas met de implementatie van model checking via binaire beslissingsbomen en de mogelijkheid om symbolische informatie op basis van modale logica in het systeem te verwerken, kon het systeem ook zeer complexe systemen verifiëren en was het relevant geworden om op brede schaal in te zetten bij computerontwerpen. Ook Microsoft gebruikt een vorm van model checking als onderdeel van haar SLAM-project om betere code op te leveren.

Reacties (22)

[CAPSLOCK2000]

Dijkstra heeft wel heel mooi bedacht dat het mooi is als je kan bewijzen dat je programma correct werkt, maar hoe je dat dan moet doen is nog een groot probleem. Hij heeft wel wat dingen bedacht om algoritmes te bewijzen enzo, maar hett is zo moeilijk en omslachtig dat het in practisch gezien onmogelijk is om een willekeurig systeem helemaal te bewijzen. Verder is het wel zo dat je kan bewijzen dat je code doet wat jij zegt dat het moet doen, maar je kan niet bewijzen dat het ook is wat jij wil dat het moet doen.

Deze kerels hebben een manier bedacht om je helpen bij het bewijzen van de betrouwbaarheid van je systeem.

PS. Begrijp me niet verkeerd, Dijkstra is een geweldige kerel.

[Reactie gewijzigd door CAPSLOCK2000 op 23 juli 2024 05:03]

[MneoreJ]

Wat Dijkstra propageerde was om het bewijs van correctheid en de constructie van het programma tegelijkertijd te doen. Dus niet eerst het programma schrijven en dan bewijzen dat het correct is (wat bijna niet te doen is voor mensen, en dus komen daar de model checkers te hulp). Dit leidt wel tot een heel andere stijl van programmeren die de meeste mensen niet leuk of praktisch vinden.

Het omgekeerde, trouwens (eerst het bewijs schrijven en daar het programma uit af leiden) klinkt helemaal bizar maar wordt ook gebruikt. Dit is de Curry-Howard correspondence: wiskundige bewijzen die programma's zijn (en omgekeerd).

Model checking is makkelijker in te passen in bestaande ontwikkelpraktijken dan bovenstaande methodes, maar dat maakt ze nog niet slecht of onbruikbaar. Alleen niet weggelegd voor de meeste ontwikkelaars (die niet zo dol zijn op veel wiskunde).

[IntToStr]

Ik heb nog gemailed met die groep tijdens mijn afstudeerproject over model checking

Er zijn verschillende tools op de markt, maar er zijn in de praktijk toch nog wel erg veel hobbels (of soms hele bergen) in de weg. Je hebt vaak de keuze tussen redelijke tools die modellen als input nemen en experimentele tools die C code kunnen inlezen. Je zult dus altijd eerst je code om moeten zetten in een model of moeten accepteren dat er van alles mis kan gaan... Het moet echt jip en janneke code zijn om te werken...

Uiteraard is het wel nuttig als je al een goed model hebt en dat kunt gebruiken. Je moet het vaak wel omschrijven. Het is dan alleen wel noodzakelijk dat er dus vanaf het begin gestructureerd wordt gewerkt en dat er echt wordt nagedacht over het ontwerp. Als je er later alsnog een zootje van gaat maken heb je er ook niets meer aan.

Erg interessante techniek. Veelbelovend ook, maar er zal toch nog wel het een en ander moeten gebeuren om het in de industie in gebruik te nemen. Zeker problemen met multithreading zullen aangepakt moeten worden; dit levert namelijk gigantische toenames in de state space op.

[Simkin]

Dit kan toch bijna oneindig complex worden? Of zit er een limiet aan het aantal niveaus (stappen) dat de transitie mag doorlopen?

[Verwijderd]

zolang het aantal states dat moet worden verwerkt in het geheugen past van de machine die de verwerking ervan doet is er niet direct een probleem vermoed ik. Je moet alleen voldoende verificatietijd kunnen aanvaarden.

Zoals het artikel zegt, wordt de implementatie getoetst aan de specificatie. Dus de specificatie moet bepalen indien het 'blijven steken in een state' gedurende 'x' aantal stappen al dan niet fout is.

dit is dus een vrij robuste test procedure en dus een prijs waardig.


je mag dit niet verwarren met zogenaamde "code coverage" testen waarbij wordt nagegaan indien elke lijn broncode (bvb hardware beschrijving in de vorm van vhdl of verilog) al dan niet wordt getriggered bij het aanleggen van de testvector. Dat geeft geen enkele garantie dat de uitgevoerde lijn ook daadwerkelijk de logische functie uitvoert die beschreven is in de specificatie.

[Reactie gewijzigd door Verwijderd op 23 juli 2024 05:03]

[latka]

Dit is altijd een afweging: sommige modelcheckers gaan als de brandweer maar vreten geheugen. Andere gebruiken minder geheugen maar zijn langzamer.

[VyperX]

Zoals het artikel zegt, wordt de implementatie getoetst aan de specificatie.
...

Dat is nou net niet wat er gebeurt bij Model Checking. Daar wordt slechts het model van het systeem/programma doorgerekend om te kijken of er fouten zitten in dat model. Pas daarna worden Testtechnieken gebruikt om "zekerheid" te krijgen dat de implementatie ook werkelijk voldoet aan het model (Conformance). Meestal is het niet mogelijk om volledig zeker te zijn of de implementatie voldoet, bijvoorbeeld als deze oneindig gedrag vertoont.

[Mic2000]

Ja dat leek mij ook. Misschien dat alles in delen opgesplitst word en per deel de mogelijkheden worden uitgerekend. Ik zou ook graag hier wat meer informatie over willen zien / lezen

[VyperX]

De meeste model checkers zijn in staat om toestanden te herkennen die zij eerder hebben gezien. Op het moment dat ze zo'n toestand bereiken weten ze dat ze die niet verder hoeven te analyseren. Ook worden er technieken gebruikt om verschillende ordeningen van acties die geen invloed hebben op het eindresultaat weg te halen (Partial Order Reduction)

Op het moment dat er enorm veel unieke toestanden zijn worden vaak benaderingstechnieken gebruikt, bijvoorbeeld door het vergelijken van hash-waardes van toestanden in plaats van het volledig opslaan van de toestand zelf.

[vgroenewold]

Ik begrijp het niet 100%. Het gaat dus over een model als ik het goed begrijp. Werk je volgens dat model (opzetten netwerk oid) dan spoor je makkelijker fouten op... ?

[IntToStr]

Je maakt een model waarin alle mogelijke keuzes in een systeem of programma kunnen worden gemaakt. Dit levert een heleboel states op waar je in terecht komt door een bepaalde actie uit te voeren. Je kunt dan met speciale formules (in temporal logic) aangeven dat je bijvoorbeeld nooit in een bepaalde state uit mag komen. De model checker controleert dan door alle mogelijke keuzes te maken of je inderdaad niet in die bepaalde state kan komen.

Op deze manier kun je eigenschappen van een systeem testen.

[Jackybeer]

Software verificatie is een garantie tot betrouwbaarheid, zelfs Microsoft gebruikt hun opsporingstechnologie voor haar Slam project.

[latka]

even de verwachtingen temperen (modelchecking was mijn afstudeerwerk): een quote van Donald E. Knuth: "Beware of bugs in the above code; I have only proved it correct, not tried it.".
Modelchecking is leuk, maar kent zijn beperkingen:
1) Je model is een vereenvoudigde versie van je programma
2) Je toests of je in een bepaalde toestand kunt komen

De problemen zijn:
1) Is je model inderdaad goed. Software is dermate complex tegenwoordig, dat de state-space van Excell veel te groot is om ooit te toetsen.
2) Je vraag moet goed zijn: stel de vraag is: kom ik ooit op de foutpagina? Dan zal je programma ook in een eindeloze lus kunnen vliegen om zo nooit in de fout te gaan. M.a.w. je programma komt nooit in de foutpagina maar 'hangt'.

Vooral het eerste probleem (het aantal toestanden) is een bottleneck voor real-life software. Een algoritme lukt nog wel, de rest wordt behoorlijk lastig.

[cosmo_roel]

Uppaal is ook een voorbeeld van een leuke tool voor model checking. Wordt op de RU veel gebruikt volgens mij.

[boner]

ehm komt die eer niet eigenlijk toe aan Dykstra? Dat is toch de vader van het structured programming en bewijsbaar correct coderen?

[latka]

Model checking is eigenlijk een botte-boer methode om correctheid te bewijzen (trial and error). Dijkstra was meer van de elegante wiskundige bewijsvoering.
Overigens: 'k heb ooit meegemaaakt dat zo'n mooie elegante bewijsvoering waar 3 jaar aan gewerkt was in 15 seconden door een model-checker omgever werd gegooid: zat een foutje in het bewijs..... dat krijg je met elegante door mensen uitgewerkte bewijzen.

[MneoreJ]

Het omgekeerde komt alleen ook voor: de model checker geeft een resultaat dat niet klopt omdat er een bug in de model checker zit...

Uiteindelijk kan het elkaar alleen maar aanvullen.

[JLM2SQUARE]

Ik kan alleen maar zeggen: ' HULDE ' voor die mensen

[OpenMinded]

Wiskundig is bewezen dat het checken van foutloosheid op een programma niet mogelijk is.
Lijkt mij dus dat alleen de modellen die met software gemaakt zijn getest kunnen worden.
Maar wat is daar nieuw aan?
En als mickeysoft het gebruikt en het resultaat is Windows, dan helpt het dus geen moer :)!

[Verwijderd]

LoL, dat is een goeie .

Zowieso denk ik dat het natuurlijk wel help als je deze technieken gebruikt, maar omdat het aantal toestanden waarin de SW zich kan bevinden zo enorm groot is kun je denk ik nooit 100% bugvrije SW maken. Door gestructureerd te werken en een goede teststrategie kan je het wel een heel stuk verbeteren.
Voor HW is deze techniek denk ik beter te gebruiken imdat daar i.v.m SW het aantal toestanden veel beperkter is. Alhoewel vraag ik me met FPGA wel eens af, wat is dat nou Hardware of SW? Je kan vanalles 'programmeren' in een FPGA.

[Reactie gewijzigd door Verwijderd op 23 juli 2024 05:03]

[Collen]

Worden zo ook lekker afgezet, dacht dat je 1 Miljoen Euro kreeg als Nobelprijs winnaar
(10 Miljoen Zweedse kronen)

hun krijgen maar 250.000 dollar (200.000 euro? of is het al nog lager geworden)

[Neomess]

officieus, dus niet officieel.
Deze instantie hanteerd dus helaas voor de winnars niet de Nobelprijs prijzen.

Overigens veel van dit soort zaken op school moeten doen, ben blij dat ik er vanaf ben want dit is niet mijn soort stof.

[Reactie gewijzigd door Neomess op 23 juli 2024 05:03]