Edmund M Clarke van de Carnegie Mellon Universiteit, E Allen Emerson van de Universiteit van Texas Joseph Sifakis van de Universiteit van Grenoble kregen in totaal een bedrag van 250 duizend dollar uit handen van de Association for Computing Machinery (ACM) in New York voor het ontwikkelen van hun ' model checking' verificatietechnologie.

Enorme impact

Volgens ACM heeft het werk van de onderzoekers ervoor gezorgd dat model checking is getransformeerd van een theorie naar een volledig geautomatiseerd proces dat zowel hardware- als softwareontwikkelaar in staat stelt om foute te ontdekken binnen ingewikkelde systeemontwerpen.

Volgens Stuart Feldman, hoofd van ACM, heeft het werk van Clarke, Emerson en Sifakis een enorme impact gehad op de ontwerpers en ontwikkelaars van semiconductor chips: "Deze industrie heeft te maken met een enorm snel groeiende markt, waarin ongekend complexe producten precies moeten doen wat er van ze verwacht wordt, omdat de toekomst van bedrijven daar letterlijk van afhangt. Zonder de doorbraak van deze onderzoekers, zouden we nu nog steeds zitten met chips die velen fouten bevatten en die niet zo krachtig en snel zouden zijn als de huidige chips."

Zekerheid

De invoering van model checking als standaardprocedure voor kwaliteitsgarantie heeft IT-ontwikkelaars in staat gesteld om met behulp van berekeningen een bepaalde zekerheid te verkrijgen op het gebied van prestaties die bepaalde systemen en applicaties kunnen leveren.

De procedure wordt ook regelmatig gebruikt bij de verificatie van ontwerpen van geïntegreerde chips zoals microprocessoren, maar ook van communicatieprotocollen, apparaatstuurprogramma's, real-time embedded systems en beveiligingsalgoritmen.

Rekenfouten en hun gevolgen

Rekenfouten in het ontwerp van chips, software architectuur of communicatieprotocollen vormen een potentieel groot probleem voor systeemontwerpers. Ze kunnen leiden tot vertragingen bij het leveren van nieuwe producten, grote fouten bij bestaande producten die al in gebruik zijn, peperdure vervangingsoperaties van gebrekkige hardware en patches van gebrekkige software.

Nooit genoeg tests

"Er kan simpelweg nooit genoeg worden getest, dus iedere methode die de kwaliteit van computersystemen verbetert, zal zorgen voor meer vertrouwen in het gebruik van deze systemen. Dit zal zeker in de toekomst nog belangrijker worden, naarmate computers in steeds meer gebieden geïntegreerd raken. Het is dan van het allergrootste belang dat eventuele fouten al worden opgespoord voordat de producten daadwerkelijk in productie gaan" zegt Vinod Bhatia hoofd operations van Paragon Simulation, een bedrijf dat is gespecialiseerd in modelling.

De AM Turing Award is vernoemd naar Alan M Turing, een Britse rekenkundige die onder andere heeft bijgedragen aan het ontcijferen van het Duitse Enigma coderingssysteem tijdens de Tweede Wereldoorlog. De eerste AM Turing Award werd in 1966 uitgereikt.