A common framework for the analysis of reactive and timed systems

Dr. ir. T.A.C. (Tim) Willemse, RU

Het ontwerpen van complexe, computergestuurde systemen is moeilijk en wordt vaak niet goed begrepen. Om te kunnen garanderen dat de uiteindelijke systemen correct zijn ontworpen wordt er gebruik gemaakt van formele methoden: wiskundige technieken die het ontwerpproces kunnen ondersteunen. Model checking is zo'n populaire techniek die gebruikt wordt om het ontwerp in een vroeg stadium te analyseren. Deze techniek wordt gebruikt voor verschillende probleemdomeinen, zoals real-time, hybride, en data-afhankelijke systemen, maar waar de systemen deze probleemgebieden overstijgen is er vaak geen analyse mogelijk. Dit wordt veroorzaakt door de gespecialiseerde technieken die toegespitst zijn op dergelijke gespecialiseerde domeinen, en die maar moeilijk kunnen worden vertaald naar nieuwe domeinen. Het doel van dit project is om model checking technieken uit deze gespecialiseerde domeinen te bestuderen binnen een raamwerk, namelijk dat van de zogenaamde Parameterised Boolean Equation Systems (PBESs). Deze PBESs hebben hun nut voor model checking voor data-afhankelijke systemen reeds bewezen. Door het verenigen van technieken binnen dit raamwerk wordt het mogelijk om resultaten uit gespecialiseerde gebieden te bestuderen en eventueel te gebruiken voor andere gebieden. Naast de nieuwe inzichten die dit verschaft bieden PBESs nog een additioneel voordeel. Zo kunnen oplossingen voor sommige PBESs met behulp van patroon herkenning eenvoudig en goedkoop worden gevonden. Hoewel dergelijke technieken gemeengoed zijn binnen de wiskunde (bijvoorbeeld voor di_erentiatie van functies), zijn zij vrijwel ongebruikt bij de analyse van processen door model checking. Deze techniek, en andere PBES gerelateerde technieken moeten verder worden onderzocht en ontwikkeldvan processen door model checking. Deze techniek, en andere PBES gerelateerde technieken moeten verder worden onderzocht en ontwikkeld.