Formele methoden tillen embedded systemen naar hoger niveau

Probleem

Een bedrijf maakt liftsystemen voor zware voertuigen als treinen en trucks. De lift bestaat uit een gedistribueerd sys-teem van een aantal poten met op ieder een kleine embedded controller en bedieningsknoppen. De liftpoten moeten precies gelijk op en neer bewegen. Dat regelen die microcontrollers via een zichzelf configurerend netwerk, omdat een willekeurig aantal liftpoten tezamen een netwerk moet vormen.

In deze architectuur is het niet eenvoudig om uitbreidingen op het systeem te maken, zonder concessies te doen aan de hoge betrouwbaarheidseisen ervan.

Onderzoek

Doel van het Progress-project CES.5008 bij het Centrum voor Wiskunde en Informatica was om formele methoden in te zetten bij het ontwerpen van dit soort embedded systemen. Een formeel model is een wiskundige beschrijving van een ontwerpspecificatie. Als je die hebt dan maken tools het mogelijk om automatisch te verifiëren of het functionele gedrag van een dergelijk formeel model aan de gestelde eisen voldoet.