Formal design of industrial safety-critical systems (EIF.3959)

Complexe computer systemen, zoals die bijvoorbeeld voorkomen in treinen, vliegtuigen, procesbesturing, signaal-verwerking en proces-bewaking, spelen een steeds belangrijkere rol in de samenleving. Derhalve worden steeds hogere eisen gesteld aan de kwaliteit van deze systemen, betreffende onder meer reactietijd, beschikbaarheid, veiligheid, robuustheid, integreerbaarheid en onderhoudbaarheid van operationele systemen.
Probleem daarbij is dat de software van dergelijke systemen dermate complex is dat met de huidige technologie niet is na te gaan of zo'n systeem aan de gestelde eisen voldoet. Het aantal denkbare situatie is dermate groot dat bijvoorbeeld testen onvoldoende zekerheid geeft over de correctheid. Gezien de rol die dergelijke systemen vervullen binnen onze samenleving is dit met recht een zorgwekkende situatie te noemen. Denk bijvoorbeeld aan de gevolgen van een ontwerpfout in de besturingssoftware van een vliegtuig of trein. Om nu aan de vraag naar grotere kaliteit te voldoen is een wezenlijke verbetering van het ontwerpproces nodig. Een goed begrepen en gestructureerde aanpak tot software-ontwikkeling is noodzakelijk om systemen van de vereiste kwaliteit te kunnen vervaardigen.

Een essentieel onderdeel bij het verbeteren van het ontwerpproces is de toepassing van formele methoden, waarbij de eisen aan een systeem met mathematische precisie worden vastgelegd. Dit maakt het mogelijk de correctheid van de ontwerpstappen, en uiteindelijk van het totale systeem, formeel te verifiëren. Toepassingen van formele methoden zijn echter meestal beperkt gebleven tot relatief kleine voorbeelden, waarschijnlijk omdat ze vaak gericht zijn op het algemene software-ontwikkelprocess. Vanuit de industrie bestaat echter grote behoefte aan een uitbreiding naar grootschalige en complexe toepassingen. Bovendien is er behoefte aan methoden die zijn toegespitst op de voor de betreffende industrie relevante klasse van systemen.
In de industrie wordt een verbetering van het software-ontwerp proces dan ook vaak gezocht in het gebruik van een specifieke (software) architectuur die toegesneden is op een bepaalde klasse van systemen, gebruik makend van eigenschappen van het toepassingsdomein. Zo wordt bij een industrieel bedrijf een reductie in de complexiteit van het ontwerpproces bereikt door het gebruik van SPLICE, een gedistribueerde systeemarchitectuur. Een voordeel van SPLICE is het gemak waarmee dynamische reconfiguratie en uitbreidingen aan het systeem mogelijk zijn. Bovendien vormt het een goede basis voor het afhandelen van defecten in de onderliggende hardware en voor een flexibele aanpassing aan externe omstandigheden.

Doel van dit project is te onderzoeken hoe bovengenoemde oplossingen gecombineerd kunnen worden, dat wil zeggen, hoe een formele ontwerpmethode afgestemd kan worden op een concrete industriële architectuur. De originaliteit ligt in de directe koppeling tussen formele ontwerpmethoden, zoals die onder andere aan de Technische Universiteit Eindhoven ontwikkeld zijn, en een afgebakende klasse van industrieële toepassingen. Door uit te gaan van een generiek industrieel product, in dit geval SPLICE van een industrieel bedrijf, wordt een basis gelegd om uiteindelijk te komen tot een industieel toepasbare formele ontwerpmethode.

Gebruikers