| Het gedrag van computers wordt typisch gemodelleerd in termen van eindige automaten met toestanden en discrete overgangen daartussen. Een centraal probleem binnen de informatica is dat het aantal (bereikbare) toestanden van een realistisch systeem al snel uit de hand loopt: wanneer een programma (of hardwarecomponent) bijvoorbeeld gebruikmaakt van honderd variabelen die ieder een (geheeltallige) waarde van 0 tot en met 9 mogen aannemen, dan is het aantal bereikbare toestanden in potentie googol ($10^{100}$), veel groter dan het aantal atomen in het universum. De meeste IT-applicaties hebben veel meer dan googol toestanden. Recent is er door informatici spectaculaire vooruitgang geboekt ten aanzien van het rekenen met grote toestandsruimtes (``model checking''). Een basisidee is dat men de bereikbare toestanden niet een voor een afloopt maar rekent met (compact gerepresenteerde) verzamelingen van toestanden tegelijk. Ook is er veel onderzoek gedaan naar het automatisch construeren van abstracties. Zo kan de computer bijvoorbeeld detecteren dat de precieze waarde van een integervariabele er niet toe doet en dat het voldoende is om te weten of die positief, negatief dan wel nul is. Er zijn nu gereedschappen die abstractie en model-checking combineren om functionele eigenschappen van broncode te analyseren (bijvoorbeeld device drivers van Microsoft met meer dan 100.000 regels C code). Steeds meer software is ingebouwd (embedded) in apparaten waarvan het de functionaliteit bepaalt (copieermachines, vliegtuigen, autos, treinen). Deze embedded systemen moeten voldoen aan een groot aantal kwantitatieve eisen (geheugengebruik, energieconsumptie, real-time, enz). Alhoewel speciaal voor dit doel ontwikkelde model checkers (zoals de real-time model checker UPPAAL) inmiddels zeer effectief zijn in het doorrekenen van kwantitatieve eigenschappen van abstracte modellen, is er momenteel nog geen goed gereedschap om automatisch goede abstracties te construeren. Het doel van dit project is om zulk gereedschap te ontwikkelen: programmatuur waarmee het real-time gedrag van modellen en software voor embedded systemen geanalyseerd kan worden. Hiertoe willen we de techniek van tegenvoorbeeld gedreven abstractie verfijning ontwikkelen in de setting van real-time systemen. Deze techniek is zeer succesvol gebleken bij het analyseren van functionele eigenschappen van broncode, en is daarnaast met succes toegepast bij het analyseren van hybride (gemengd discreet/continue) systemen. Totnutoe heeft niemand tegenvoorbeeld gedreven abstractie verfijning ontwikkeld voor het analyseren van de bereikbare toestanden van real-time systemen. Dit is ook niet eenvoudig, maar wij denken dat het mogelijk is en verwachten dat het zeer effectief zal zijn. Allereerst willen we een prototype gereedschap ontwikkelen gebruikmakend van een bestaand pakket voor het manipuleren van Difference Bounded Matrices (DBMs), een datastructuur die een essenti\"ele rol speelt in bestaande real-time model checkers. Na evaluatie en fine tuning van het prototype op basis van een aantal standaard benchmarks willen we, in samenwerking met collega's van de universiteit van Aalborg, de techniek toevoegen aan UPPAAL, een state-of-the-art model checker voor real-time systemen. We willen daarbij proberen om de door ons ontwikkelde abstractie verfijning voor real-time gedrag (DBMs) te combineren met de bestaande abstractie verfijning voor discrete toestandsruimtes. Vervolgens willen we de techniek evalueren middels toepassing op industriële real-time UML modellen. |
