Joost-Pieter Katoen is hoogleraar softwaremodellering en -verificatie aan de RWTH Aachen. Viet Yen Nguyen is onderzoeker bij diens groep.

27 December 2012

Het Esa-project Compass beoogt een geïntegreerde, coherente aanpak te ontwikkelen voor het ontwerp en de analyse van ruimtevaartsoftware. In dit artikel geven de betrokken onderzoekers van de RWTH Aachen een impressie van de gekozen benadering en de resultaten.

De Ariane 5-raket, het Mars-karretje Curiosity, het internationale ruimtestation ISS, de Hubble-telescoop, allemaal ruimtevaartsystemen die tot de verbeelding spreken. Het ontwerp ervan is een enorme onderneming. We hebben het dan niet zozeer over de imposante fysieke gestalte van dergelijke satellieten, raketten of robots, maar met name over de software.

Waar software in de jaren tachtig slechts een bescheiden rol speelde, zijn moderne systemen bijna vliegende computerprogramma‘s. De Voyager 1 in 1977 bevatte bijvoorbeeld maar twee kilobyte aan code, de Mars Pathfinder in 1997 al 175 KB. Deze groeitrend is exponentieel.

Aan de hand van het systeemmodel, inclusief foutinjecties, genereert de Compass-toolset zogeheten foutbomen.

Tegelijk levert de moderne besturingssoftware een ongekende nauwkeurigheid en betrouwbaarheid. Maatregelen als redundantie, foutdetectie en -correctie maken verre interplanetaire verkenningsmissies mogelijk. Daarnaast zorgen nauwkeurigere algoritmes voor strakkere vluchtbanen, waardoor navigatiesystemen zoals GPS locaties met centimeterprecisie kunnen bepalen. Het gaat dus om uiterst kritieke software.

Een rigoureus verificatie- en validatietraject houdt de risico‘s, correctheid en functionaliteit van deze complexe software binnen strikte grenzen. Toegesneden ontwerp- en analysetechnieken gaan na of bijvoorbeeld de softwarearchitectuur, redundantiestrategieën en protocollen afdoende zijn. Het arsenaal is in de loop der jaren flink gegroeid: peerreviews en uitgebreide testprogramma‘s om de softwarekwaliteit te garanderen, wachtrijtechnieken en simulaties om iets te kunnen zeggen over de efficiëntie, foutbomen en FMEA-tabellen om de causale verbanden tussen fouten in componenten en in systeemonderdelen te benadrukken en te kwantificeren en Matlab/Simulink om continue processen te simuleren, zoals temperatuur- en energieregeling – uitermate belangrijk voor apparaten die bijna volledig zijn aangewezen op zonne-energie.

Maar hoe is de consistentie tussen de verschillende analyseresultaten gewaarborgd? Wat is de relevantie van een lage foutkans in een foutboomanalyse als het model waarop deze analyse is gebaseerd de belangrijkste efficiëntiebottlenecks buiten beschouwing laat? Hoe kan een simulatie van de drukregeling in een raket betrouwbaar zijn als het onderliggende model essentiële componenten van de besturingssoftware niet in detail meeneemt?

Deze vragen waren voor Esa reden een programma te initiëren om een geïntegreerde, coherente aanpak te ontwikkelen. In 2008 zijn wij deze uitdaging aangegaan. Met de Embedded Systems-groep van het Italiaanse onderzoeksinstituut Fondazione Bruno Kesler en de RD-afdeling van ‘s werelds grootste satellietproducent Thales Alenia Space hebben wij onze krachten gebundeld in het Europese Compass-project (Correctness, Modeling and Performance of Aerospace Systems, zie kader).

Honderd procent betrouwbaar

Als uitgangspunt voor de modellering hebben we de Architecture Analysis Design Language (AADL) genomen. Deze (merendeels) door de automobielindustrie en de lucht- en ruimtevaartsector ontwikkelde en inmiddels gestandaardiseerde modelleringstaal ondersteunt de beschrijving van software- én hardwarecomponenten, zoals processoren, communicatiebussen, multithreads en processen. Dat kan zowel in een tekstuele als in een grafische notatie.

AADL maakt een duidelijk onderscheid tussen interface en intern gedrag. Het gedrag van componenten modelleren we met behulp van automaten, terwijl we de hiërarchie kunnen representeren als een eenvoudige variant van de bestaande hiërarchie in UML-toestandsdiagrammen. Componenten kunnen dus diverse subcomponenten hebben, oftewel: details zijn op diverse niveaus te beschrijven.

Een componentmodel in AADL bestaat in feite uit twee delen: het nominale en het errorgedrag. Het nominale gedrag beschrijft hoe de component zich gedraagt als er geen fouten optreden. Dit is doorgaans deterministisch. Het errorgedrag geeft aan met welke frequentie fouten kunnen optreden. De koppeling van beide delen maakt het mogelijk voor een fout aan te geven welke invloed deze heeft op het systeemgedrag. Dit heet ook wel foutinjectie.

Een belangrijke feature van AADL is de mogelijkheid om dynamische connecties te leggen tussen componenten. Hierdoor kunnen bij het uitvallen van systeemcomponenten redundante tegenhangers hun taak direct overnemen, waarbij ze meteen op de juiste manier zijn verbonden met het resterende systeem. Binnen het Compass-project hebben we hier een aantal mogelijkheden aan toegevoegd. Zo zijn continue variabelen zoals temperatuur en druk nu te beschrijven met (eenvoudige) differentiaalvergelijkingen en fouten te modelleren met stochastische modellen.

Hoewel deze uitbreidingen in de praktijk relevant blijken, is een andere bijdrage wellicht nog belangrijker: we hebben AADL uitgerust met een formele semantiek. Met andere woorden: we hebben een precieze, wiskundige interpretatie gegeven aan wat we in (de uitgebreide versie van) de taal kunnen modelleren. Het belang hiervan is niet alleen wetenschappelijk. Sterker nog: in onze filosofie kunnen we betrouwbare analyses alleen uitvoeren als we precies vastleggen welk wiskundig model eraan ten grondslag ligt.

Het heeft even geduurd om de geldschieter en de industriële partner in het project hiervan te overtuigen en het heeft ook geleid tot een eenmalige kleine vertraging, maar zoals zo vaak komt het zoete achteraf: de analyses zijn honderd procent betrouwbaar. Zo stelden we aanvankelijk een fout in de foutboomanalyse vast, die uiteindelijk echter bij een commerciële tool bleek te liggen die we ter vergelijking gebruikten. Kortom: investeren in een formele semantiek loont zeker de moeite.

De Compass-toolset biedt een volledig grafische schil, met een klik-en-sleepomgeving om modellen te construeren.

Klik-en-sleepomgeving

Het gedrag van het hele systeem en zijn software doorgronden we met verschillende analyses. Het begint met functionele correctheid. Met simulatie- en model-checkingtechnieken controleren we of het systeem de functionele requirements naleeft. Aan de hand van het systeemmodel, inclusief foutinjecties, genereert onze tool vervolgens foutbomen en FMEA-tabellen (failure mode and effects analysis). Deze automatisering bespaart de ingenieurs veel werk, aangezien zij de analyses in de huidige praktijk handmatig uitwerken. Uit een complex AADL-model voor een moderne satelliet hebben we bijvoorbeeld foutbomen van ongeveer zeventig elementen volledig automatisch gegenereerd. Het is een hele klus om dit secuur met de hand te doen.

Onze tool kan ook de uitvalskansen berekenen van kritieke gebeurtenissen, zoals een zonne-eclips of stralingsdefecten aan de zonnepanelen. Daarnaast is het foutbeheersingssubsysteem tot in de puntjes door te lichten. Het gereedschap gaat na of er voldoende sensoren aanwezig zijn in het ontwerp om specifieke fouten te herkennen. Het rekent tevens uit welke sensoren worden geactiveerd bij een foutinjectie en relateert dit in de vorm van een foutboom. Ten slotte bepaalt het of de herstelstrategie, gegeven een geïnjecteerde fout, slaagt.

Ten grondslag aan deze analyses liggen de modernste, in eigen huis ontwikkelde model-checkers NuSMV en MRMC. Aan de hand van de formele semantiek rekent NuSMV alle bereikbare toestanden uit, om vervolgens de gewenste foutbomen, FMEA-tabellen en verificatierapportages te extraheren. Deze toestandsruimte groeit explosief. Enkele biljoenen toestanden is geen uitzondering. Symbolische representaties, slimme minimalisatietechnieken en geavanceerde algoritmes houden deze gigantische omvang behapbaar voor een gemiddeld workstation.

Voor de stochastische analyses hebben we een brug geslagen tussen NuSMV en MRMC. MRMC rekent kansen uit zoals de waarschijnlijkheid dat de druk in een raket binnen twee uur een kritiek niveau aanneemt. Dit doet de tool met een geavanceerde combinatie van model-checking en numerieke algoritmes uit de lineaire algebra.

Het geheel is volledig grafisch te bedienen, met een klik-en-sleepomgeving om de modellen te construeren. Requirements specificeren we met behulp van patterns, in feite zinnen in natuurlijke taal waarin de ingenieurs alleen kleine wijzigingen hoeven aan te brengen. Dit zorgt voor een aanmerkelijke verlaging van de drempel om zulke eisen op te schrijven.

Enorme helderheid

Thales Alenia Space heeft het AADL-dialect en de analysetoolset die de modellen verwerkt intensief geëvalueerd vanuit een industrieel perspectief. Dit is gebeurd aan de hand van diverse cases, waaronder de temperatuurregeling van enkele satellietsubsystemen. De resultaten waren zo bemoedigend dat het licht op groen ging voor vervolgonderzoek. Hierin staat een nieuwe grote casestudy centraal: het modelleren en analyseren van een satelliet die momenteel in ontwikkeling is voor een missie die in de komende jaren wordt gelanceerd.

Parallel aan deze Esa-missie hebben we in zes maanden een eigen satellietmodel gebouwd en geanalyseerd. Dit model omvat bijna negentig systeemcomponenten en twintig foutmodellen. Het telt een kleine vijftig miljoen nominale toestanden, een aantal dat nog een factor tien tot tweehonderdduizend groter wordt afhankelijk van welke fouten we injecteren. Het modelleren is een eenmalige investering; de analyses doet de toolset daarna automatisch.

Terwijl de ingenieurs de validatie uitvoerden met de gebruikelijke technieken, hebben wij ons gereedschap ingezet. De conclusie is veelbelovend. In het bijzonder levert de enorme mate van automatisering van onze analyses een substantiële tijdwinst op. Daarnaast scheppen de formele technieken in een vroeg stadium (nog voor de codegeneratie) enorme helderheid in het systeemgedrag.

Vijf jaar intensief onderzoek heeft aangetoond dat formele methoden, in dit geval een AADL-dialect met een precieze interpretatie plus een heel scala aan geautomatiseerde state-of-the-art analyses, dergelijke praktische softwarevraagstukken in de ruimtevaartindustrie kunnen aanpakken. Ons project heeft inmiddels de aandacht getrokken van verschillende buitenlandse instanties (met name ook buiten de EU). Daarnaast heeft het geleid tot de lancering van verschillende vervolgprojecten voor de Esa en tot diverse nieuwe wetenschappelijke onderzoeksvragen.

Edited by Nieke Roos