Het ontwerpen van zgn. real-time systemen, waarbij het functionele gedrag van een systeem afhankelijk is van tijdsaspecten, is een complexe aangelegenheid. Het laatste decennium is daarom veel aandacht gegeven aan het ontwerpen van theorie en gereed- schap om dit ontwerp te ondersteunen. Een succesvol paradigma is het zgn. timed automata model, dat gebaseerd is op automaten uitgebreid met klokken. Een systeem kan worden gemodelleerd met behulp van dit model, waarna met behulp van comput- ergereedschappen diverse correctheidseigenschappen geverifieerd kunnen worden. Deze gereedschappen hebben inmiddels een grote rijpheid bereikt en kunnen op industriele schaal worden toegepast.

Een probleem is dat het timed automata model uitgaat van een oneindige precisie van klokken en systeemparameters. In een implementatie zullen klokken en parameters altijd een zekere onnauwkeurigheid hebben, wat ertoe kan leiden dat dat een implemen- tatie zich wezenlijk anders gedraagt dan het geverifieerde model. Dat kan tot gevolg hebben dat een correct bevonden systeemontwerp incorrect gedrag vertoont wanneer het uiteindelijk geimplementeerd wordt, wat uiteraard een verontrustend probleem is. Vandaar dat dit project zich richt op het onderzoek van de robuustheid van systemen, dwz. de eigenschap dat een systeem voor bepaalde eigenschappen (zoals correctheid) ongevoelig is voor kleine verstoringen in klokwaarden en systeemparameters. Daarnaast richt het project zich op technieken en gereedschappen om robuustheid te bewerkstelli- gen. Naast deze praktisch gemotiveerde doelstellingen beoogt dit project te komen tot een omvattende theorie van cyclisch gedrag, die zijn diensten kan bewijzen in verwante gebieden als real-time testen, hybride systemen en het versnellen van model checking algorithmes.

Summary in English