Pientere machines; Ingebouwde software maakt apparaten steeds slimmer

Scheerapparaten, auto's, telefoons en vliegtuigen hebben steeds meer ingebouwde computersystemen. Handig, maar een programmeerfout zit in een klein hoekje.

STEEDS MEER levert de mens zich uit aan intelligente apparaten. Hun ingebouwde hardware en software (embedded system) controleert bij een scheerapparaat de batterij, om bevind van zaken te geven via een display. Bij mobiele telefonie, waar de programmatuur uit miljoenen regels bestaat, zoekt het apparaat automatisch het dichtstbijzijnde basisstation en om de batterij te sparen is de signaalsterkte niet meer dan strikt noodzakelijk. Vaak gaat het om systemen die met sensoren hun omgeving continu aftasten en in real time opereren: het vinnetje van een vliegtuig moet binnen een oogwenk om, anders hoeft het niet meer.

Apparaten met ingebouwde software zijn een groeimarkt. Het aantal kilobyte aan programmatuur dat erin is verwerkt stijgt exponentieel en kwam de consument in 1985 dagelijks met één microprocessor in aanraking, vorig jaar waren dat er vijftig. Vaak zie je een microprocessor eerst (goedkoper) een bestaande functie overnemen, bijvoorbeeld het zoeken van een radiostation, waarna een creatieve geest extraatjes bedenkt, zoals het 'vasthouden' van de laatst ingestelde zender. Binnen de automobielindustrie is de verwachting dat binnen enkele jaren 20 procent van de kosten van een middenklasser voor rekening komt van informatietechnologie aan boord. De eerste gloeilamp met microprocessor lijkt niet ver meer weg.

CONGRES

Hebben we in het algemeen veel vertrouwen in slimme apparaten, soms gaat het mis. Een fout in de Pentium processor heeft het Amerikaanse bedrijf Intel in 1994 naar schatting 200 miljoen dollar gekost. Tijdens de Golfoorlog was het een softwarefout die belemmerde dat een Patriotraket een Iraakse Scud kon onderscheppen, met als gevolg een vernietigende inslag in een barak met Amerikaanse troepen. Toen in 1990 een subtiele softwarefout zich razendsnel over de centrales van AT&T verspreidde en het telefoonverkeer in heel Amerika lamlegde, betekende dat voor het bedrijf een schadepost van 60 miljoen dollar. Meer rampen als gevolg van disfunctionerende software staan beschreven in het onlangs verschenen boek Fatal Defect: Chasing Killer Computer Bugs van Ivars Peterson.

Over embedded systems, met speciale aandacht voor de samenwerking op dit gebied tussen de academische wereld en het bedrijfsleven, organiseerde het Instituut voor Programmatuurkunde en Algoritmiek, samen met collega-onderzoeksscholen uit Denemarken en Finland, afgelopen week in Veldhoven een congres. In het IPA participeren zeven universiteiten en het Centrum voor Wiskunde en Informatica te Amsterdam. Doel is de betrouwbaarheid, prestatie, snelheid en flexibiliteit van software te verbeteren, via fundamenteel onderzoek van promovendi en 'quick scan' derde-geldstroomprojecten.

Een manier om software van fouten te vrijwaren is formele verificatie. In Nijmegen legt de groep Informatica voor Technische Toepassingen van prof.dr. F.W. Vaandrager (mede-organisator van het congres) met deze methode zich toe op het 'correct bewijzen' van real time software, waarbij het essentieel is dat bepaalde taken binnen een vooraf bepaalde tijdsduur worden uitgevoerd. Vaandrager: “Van sommige computerprogramma's is de correctheid niet zonder meer in te zien. Die werken op een getructe manier, met processoren die elkaar berichten versturen. Dat geeft een combinatorische explosie: 40 bitjes die op 0 of 1 kunnen staan maken 2 mogelijke toestanden, dat loopt enorm uit de hand. Uitputtend zoeken met brute force helpt dan niet, alleen slimme wiskundige technieken kunnen nog bewijzen dat het programma de gewenste eigenschappen bezit. Intel en AT&T, door ervaring wijs geworden, hebben speciale instituten in het leven geroepen om zulke algoritmes te maken.”

Dergelijke tools maken gebruik van temporele logica, een wiskundige taal ontwikkeld door de Israeliër Amir Pnueli (die daarvoor begin volgend jaar de Turing Award ontvangt, de hoogste wetenschappelijke onderscheiding binnen de informatica). Het is logica waarin tijd is verwerkt, bijvoorbeeld in de vorm van beperkende voorwaarden. Op het congres in Veldhoven liet prof.dr. Al Mok van de Universiteit van Texas zien hoe op grond van een dergelijke logica een goed functionerende real time scheduling kan worden ontworpen voor de computerbesturing van de nieuw te bouwen Boeing 777. Het correct-bewijzen van deze programmatuur is geen overbodige luxe: begin 1992 stortte in Frankrijk een Airbus neer door een softwarefout.

Al valt het falen toe te schrijven aan een paar foutieve bits, meestal ligt de eigenlijke oorzaak van de ramp elders. Vaandrager: “Tussen de geledingen binnen een projectteam zijn de verantwoordelijkheden soms slecht geregeld, of men heeft er een rommelige programmeerstijl op na gehouden waar discipline is geboden. In het geval van de Therac, een computergestuurd bestralingsapparaat van het East Texas Cancer Center, ontaardde de programmatuur uit gemakzucht in een enorme brij waarin niemand nog de weg wist. Op die manier konden er slordigheden in de besturingssoftware sluipen, die ertoe leidden dat enkele patiënten dodelijke stralingsdoses kregen toegediend.”

BRUUSK

Het debâcle met de Ariane 5, de nieuwe Europese draagraket die op zijn maiden vlucht afgelopen juni 39 seconden na de start op bevel van de boordcomputer een bruuske koerswijziging van meer dan 20 graden inzette en jammerlijk verongelukte, is het ultieme voorbeeld van hoe knullig falen van software honderden miljoenen guldens schade kan opleveren. Volgens de officiële onderzoekscommissie was er sprake van een programmeerfout. Programmatuur van de Ariane 4 was overgeheveld naar de Ariane 5, onder het motto: afblijven, het werkt. Over het hoofd werd gezien dat de BH-waarde, een vertaling van de horizontale snelheid, in geval van de Ariane 5 een vijf keer zo groot getal opleverde - te groot voor het aantal beschikbare bits. Dus kreeg de centrale boordcomputer onzindata aangeleverd, die hij niettemin voor vluchtgegevens hield.

Volgens de Franse informaticus Gérard le Lann is het falen van de Ariane 5 geen softwarefout maar het gevolg van gebrekkige system engineering. “Waar het aan ontbrak was een ordentelijke lijst van specificaties”, aldus Le Lann in Veldhoven. “Die horen, inclusief dimensionering, vooraf te worden opgesteld, zodat de software-mensen weten waar ze rekening mee hebben te houden. Maar in de praktijk zijn de specificaties bij dit soort grote industriële projecten als gevolg van tijdsdruk of uit geldgebrek informeel, onvolledig en niet zelden onderling strijdig. Hoe had een programmeur dat van die horizontale snelheid moeten weten als hij geen lijst van specificaties heeft?”

Vaandrager kan zich in de conclusie van Le Lann vinden maar wijst erop dat het maken van een specificatielijst niet eenvoudig is. “Dat zijn extreem lange documenten en een uitputtende verificatie vergt veel tijd. Vaak is de gedachte: we komen er wel mee weg, tot het fout gaat. Software engineering mensen aan de universiteiten varen wel bij rampen als die met de Pentium of de Ariane 5.”

Een probleem voor de informaticus bij dit soort zaken is dat hij een duizendpoot moet zijn. Vaandrager: “De opkomst van de embedded systems noopt tot een bezinning op de breedte van de informatica-opleiding. Een informaticus is geen bepuiste hacker op een zolderkamertje. Hij moet in een team kunnen samenwerken en in de Nijmeegse opleiding, maar ook elders, is daar ruim aandacht voor. Een probleem is de vierjarige cursusduur. Een technisch-gerichte informaticus hoort schema's te kunnen lezen en met ingenieurs te kunnen communiceren. Daarom moet zijn opleiding ook veel wiskunde en natuurkunde bevatten. Anders loop je het risico dat in projecten als dat van de Ariane het overgrote deel van het programmeerwerk aan fysici en astronomen wordt overgelaten. Al kunnen ze het minder goed, ze spreken de taal.”