Arm is energiezuinig en tegenwoordig ook krachtig genoeg om de concurrentie met X86 aan te kunnen in een tradtioneel Intel-domein als embedded computers. Een rondgang langs leveranciers leert echter...
Nu politici en beleidsmakers hun aandacht hebben gericht op het oplossen van de crisis en de naderende megabezuinigingen schuift het...
Als het van de initiatiefnemers van het Greentouch-consortium afhangt (www.greentouch.org), zullen we binnen tien jaar duizend keer energie-efficiënter kunnen ‘surfen’. Een mooie maar noodzakelijke...
9 april 2008
Het Duitse Nanda Technologies maakt apparatuur die halfgeleiderwafers controleert. Om de embedded software zonder problemen te laten werken, gebruikte het bedrijf ontwerpgereedschap van Verum, dat code genereert met behulp van formele verificatie. De ongeveer 25 duizend regels C# die de ASD-tool produceerde, waren direct foutloos en in twee weken tijd geïntegreerd.
Het ontwikkelen, testen en opsporen van fouten in software is vaak een tijdrovende en kostbare zaak. Bovendien kunnen onvolkomenheden in het ontwerp een enorme schadepost opleveren in toepassingen waarin de programmatuur een cruciale rol speelt, bijvoorbeeld in embedded systemen. Het Duitse bedrijf Nanda Technologies, maker van inspectieapparatuur voor halfgeleiderwafers, was op zoek naar een techniek om snel en betrouwbaar software voor zijn complexe embedded systemen te ontwerpen.
Het Eindhovense Verum heeft een methode bedacht en bijbehorende tooling ontwikkeld die volledig aan deze wensen voldoen. Een belangrijk aspect van het Analytical Software Design-gereedschap is dat het de code automatisch genereert. In ongeveer twee weken tijd heeft Nanda de code van het hele systeem vertaald van C++ naar C#. De meeste tijd is gaan zitten in het omzetten van handgeschreven C++-wrappers. De C#-codegenerator vond hierbij voor het eerst commerciële toepassing.
Het in München gevestigde Nanda Technologies maakt apparatuur om afwijkingen in gefabriceerde wafers te detecteren. De kwaliteit van de embedded software is daarbij cruciaal. Gebruikers plaatsen het inspectiesysteem in de regel immers in het productieproces, waardoor het extreem betrouwbaar moet werken om maximale uptime te ondersteunen. Omdat dit systeem in waferfabs moet gaan draaien, was het voor Nanda erg belangrijk dat het de machine direct goed en betrouwbaar werkend aan afnemers kon aanbieden.
In nauwe samenwerking hebben Nanda en Verum de supervisory machine control-software (SMC) voor het nieuwe systeem ontworpen en geproduceerd. Hierbij hebben we gebruikgemaakt van de Eindhovense Analytical Software Design-methode (ASD) voor het vastleggen van de specificaties, de architectuur en het design. De bijbehorende tooling biedt een eenvoudige, algemeen toepasbare manier voor het ontwikkelen van mathematisch geverifieerde software. Voor het waferinspectiesysteem hebben we ASD gebruikt om code te ontwikkelen voor alle lagen in de software: van de onderste laag, die direct de hardware aanstuurt, tot aan de programmatuur voor de grafische gebruikersinterface. Het gereedschap heeft ongeveer 25 duizend regels C# gegenereerd, gegarandeerd zonder bugs.
In nauwe samenwerking met Verum heeft Nanda Technologies de ASD-tooling gebruikt om de supervisory machine control-software te ontwikkelen voor een nieuw waferinspectiesysteem.
Om de applicatie te kunnen bedienen, heeft Verum ook een test-GUI gemaakt. Bijzonder aan deze interface is dat we de GUI-controller ook met behulp van de ASD-methode hebben gemaakt. Deze besturing zorgt ervoor dat de juiste knoppen op het juiste moment worden geactiveerd. Ook voor de GUI garandeert ASD dat er geen bugs in zitten en dat het onmogelijk is om het waferinspectiesysteem iets te laten te doen dat niet is toegestaan.
In het verleden hebben we voor het waferinspectiesysteem van Nanda al eens een ontwerp gemaakt met het ASD-gereedschap. Daarbij hebben we toen C++-code gegenereerd. Dit verliep buitengewoon snel en soepel. ‘De enige problemen die we tegenkwamen tijdens het integratieproces waren bugs in de handgeschreven code’, vertelt Raghuveera Ravinutala, systeemarchitect bij Nanda. ‘In de door ASD gegenereerde code vonden we geen enkele fout.’
Nanda had de wens deze C++-code om te zetten naar C#. Verum heeft hiervoor de codegenerator uitgebreid, zodat deze C# kan produceren voor het hele design. De complete applicatie bestaat nu alleen nog uit C#-code. Het grote voordeel hiervan is dat alle handgeschreven wrappercode niet meer nodig is, zodat ook de bugs zijn te elimineren in de eerder met de hand geschreven code. De wrappers zijn noodzakelijk om C#-types om te zetten naar C++-varianten en andersom.
Met een doorlooptijd van drie weken hebben we de codegenerator geverifieerd, de code opnieuw gegenereerd, getest en volledig werkend geïmplementeerd. Het meeste werk zat in het omzetten van handgeschreven C++-code. Hiervoor hebben we eerst een ASD-design gemaakt, waarna we de C#-code automatisch konden genereren. Ook enkele verzoeken van Nanda voor verandering van de applicatie hebben we in deze periode aangebracht.
De codegenerator neemt het grootste deel van de programmeerregels voor zijn rekening en bespaart veel tijd. Handmatig programmeren zou zeer waarschijnlijk ook bugs introduceren. Grote softwareprojecten als dit beslaan immers tienduizenden regels code. Een ander voordeel is dat de ontwikkelaar wijzigingen snel en gemakkelijk kan doorvoeren. Ook hierbij is de kans op fouten met een codegenerator aanzienlijk kleiner. De geproduceerde code heeft ook uitgebreide tracingfunctionaliteit, waardoor problemen snel en gemakkelijk zijn op te sporen.
‘Voor ons was het een groot voordeel dat we de hele applicatie in C# konden implementeren, aangezien de meeste third party-componenten, opgebouwd in meerdere manjaren, al in C# zijn geschreven’, zegt Andreas Sittinger, principal system engineer van Nanda. ‘Voor ons was de eerste C++-gebaseerde oplossing daarmee een overgangsfase en we zijn dan ook blij dat Verum de C#-codegenerator op tijd klaar had. Na de drie weken die nodig waren voor de systeemintegratie konden we al snel complete machinetoestanden testen en voor het eerst een wafer door alle stadia heen sturen.’
Door software te bouwen met behulp van formele verificatie kunnen ontwikkelaars controleren of een ontwerp correct volgens de van tevoren opgegeven specificaties is geïmplementeerd. Daarnaast geeft deze methode precies aan of de code kan vastlopen (deadlocks) of in een eindeloze lus terecht kan komen (livelocks). Verder controleert de tooling of de code in een toestand iets kan doen dat volgens de interfacespecificatie niet is toegestaan (zie kader voor de technische details).
Ook de GUI-controller garandeert een foutloze werking.
Deze manier van software ontwikkelen bespaart veel kostbare tijd die anders verloren gaat bij het debuggen en integreren van de software. Hetzelfde geldt voor het nazorgtraject. Dankzij deze methode kunnen ontwikkelaars alle problemen in het dynamische gedrag van de software al tijdens de ontwikkeling oplossen en uitsluiten dat fouten tijdens de integratie of zelfs na de release pas boven water komen. Dit leidt in de praktijk tot een softwaresysteem met een tienmaal hogere kwaliteit (gemeten in defecten per duizend regels code) dan conventioneel ontwikkelde software.
Software bestaat meestal uit verschillende componenten, gemaakt door verschillende ontwikkelaars. Bij het uitbesteden van programmatuur is het probleem dat componenten vaak niet op de juiste manier met elkaar samenwerken. Specificaties van de interface zijn onduidelijk en onvolledig. Zonder een formele verificatiemethode is het nagenoeg onmogelijk te garanderen dat een component zich ook aan deze interfacebeschrijving houdt. Voor Nanda hebben we de software volledig op afstand ontwikkeld en alleen voor de specificatie zijn we fysiek bij elkaar gekomen.
Vaak is het ontwikkelen van multithreading-applicaties (waarbij meerdere stukken van de code gelijktijdig worden uitgevoerd) erg lastig en vereist het veel specifieke kennis over threading. De gegenereerde code is volledig vrij van deadlocks en race conditions. Het is niet nodig om zelf multithreading-mechanismes te programmeren. De code daarvoor komt namelijk uit de generator. Zonder formele verificatie is het zelfs voor de meest ervaren ontwikkelaars bijna onmogelijk om software te schrijven die vrij is van deadlocks. Met deze methode kan elke programmeur een goed werkende multithreading-applicatie maken.
ASD sluit volgens Verum precies aan bij de manier van werken van softwareontwikkelaars, zonder dat zij te maken hebben met de ingewikkelde procesalgebra die ten grondslag ligt aan de gebruikte formele verificatiemethodes. De formele verificatie garandeert dat de code functioneel correct is. Het ontwikkel- en testtraject kan daardoor aanzienlijk korter, zodat het product sneller op de markt is te brengen en voldoet aan alle ontwerpeisen.
Bijzonder aan de ASD-tooling is de combinatie van formele verificatie en codegeneratie. Hierdoor is niet alleen te garanderen dat het design goed is, maar ook dat de implementatie correct is. In de praktijk genereert het gereedschap tot wel 90 procent van de code, wat leidt tot een factor 10 verhoging van de kwaliteit. Aangezien de codegenerator verschillende programmeertalen ondersteunt, is een bijkomstig voordeel dat er gemakkelijk kan worden overgeschakeld naar een andere taal.
Carlo van Asma is consultant bij Verum.
De mathematische methode die Verum heeft ontwikkeld, Analytical Software Design (ASD) geheten, maakt voor iedere softwarecomponent een zogeheten sequence-based specification (SBS). Deze wordt automatisch vertaald naar de procesalgebra Communicating Sequential Processes (CSP), die het mogelijk maakt om (software)systemen formeel te specificeren en te verifiëren. Een model-checker controleert of het gemodelleerde systeem voldoet aan de gestelde eisen. Vervolgens kan de codegenerator alle code genereren. Een specifiek kenmerk van ASD is dat de methode de CSP-algebra automatisch genereert en dat de gebruiker van de tool nauwelijks kennis van CSP hoeft te hebben. De huidige codegenerator kan zowel C# als C++ produceren. Ondersteuning voor Java is vrijwel klaar.
Voor iedere softwarecomponent maakt ASD een sequence-based specification (SBS). De codegenerator produceert code in C# of C++. Kennis van CSP, de taal om procesalgebra te beschrijven, is niet nodig.
© Bits & Chips | Deze pagina op internet: http://www.bits-chips.nl/nieuws/achtergrond/bekijk/artikel/verum-genereert-formeel-geverifieerde-c-code-voor-waferinspectiesysteem.html
