Detailed project information

Verificatie van systemen is een belangrijk onderwerp: om aan te tonen dat een systeem aan zijn specificatie voldoet worden modellen gemaakt en vervolgens met behulp van computers geanalyseerd, bv. door middel van model checkers en theorem provers. Er is uitgebreid onderzoek over klassen van modellen, daarbij behorende algoritmes en daaruit voortkomende tools. Op het gebied van het modelleren is echter een grote achterstand. De meeste modellen worden vrij adhoc geproduceerd. Er zijn geen standaardeisen aan model ontwikkeling zoals in andere disciplines. Duidelijke nadelen zijn dat over de kwaliteit van modellen weinig te zeggen is, verschillende modellen van hetzelfde systeem nauwelijks, en ook resultaten die uit verschillende tools komen moeilijk vergelijkbaar zijn. Het is duidelijk dat de kwaliteit van het hele vericatie process berust op de kwaliteit van beide onderdelen, het modelleren en de computerondersteunde analyse. In het project gaat het om het ontwikkelen van een methode voor het modelleren van embedded systems.

Modellen moeten hier vaak een controllermodel (software en hardware) met een model van de te besturen fysieke omgeving (bvb. een fabriek) verenigen. Het onderzoek richt zich hierbij op het:

verzamelen en structureren van specifieke kwaliteitseisen aan verificatiemodellen voor embedded systems, opstellen van checklijsten voor modeleigenschappen, het herkennen en beschrijven van patronen voor bepaalde klassen van systemen en modellen, door middel van case studies, vergelijk met modelleringsmethoden in verwante gebieden, bv. voor softwaresysteemen. verzamelen van geschikte representatie- en documentatievormen van modellen, systematiek voor het modelleringsprocess.