AM Turing Award uitgereikt aan ontwikkelaars model checking
Gepubliceerd: Woensdag 6 februari 2008
Auteur: Martin Gijzemijter
De AM Turing Award voor innovatie op het gebied van informatietechnologie is uitgreikt aan een groep academici die zich bezighouden met het onderzoeken van manieren om fouten in complexe hardware en softwaresystemen te reduceren.
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.
