Stepwise Refinement of Hybrid Systems

Hybride systemen zijn systemen die bestaan uit zowel discrete (digitale) als continue componenten, typisch computersystemen die in interactie staan met hun fysieke omgeving. Door de razendsnelle ontwikkelingen op het terrein van Informatie en Communicatie Technologie, komen zulke systemen meer en meer voor in een veelheid van toepassingsdomeinen, variërend van luchtvaart en procesbesturing tot robotica en consumentenelectronica. De specificatie, het ontwerp en de analyse van hybride systemen vereisen een synthese van ideeën, concepten, wiskundige theorieën en gereedschappen die momenteel verspreid zij over afzonderlijke disciplines, met name Informatica en Systeem- en regeltheorie. Immers, het is alleen mogelijk om zinvol te redeneren over de correctheid van het computersysteem wanneer men tevens een model heeft van het fysische proces dat door dit systeem bestuurd wordt, en omgekeerd.

Het doel van dit project is om (1) een methodologie te ontwikkelen voor stapsgewijze verfijning van hybride systemen, waarmee men kan aantonen dat het ene hybride model een verfijning is van het andere, en (2) het vinden van modelklassen die op algorithmische wijze geanalyseerd kunnen worden. Om dit doel te bereiken zullen binnen het project een aantal case studies aangepakt worden op het terrein van ingebouwde systemen waarbij sprake is van een niet-triviale interactie tussen discrete en continue componenten.

In 1999 heeft het onderzoek zich met name gericht op het combineren van de zgn branch-and-bound technieken bekend uit de scheduling theorie, met model checking tools voor getimede automaten, en het toepassen van deze technieken op schedulingproblemen in de staalfabriek van het Belgische Sidmar (Case Study 5 van het VHS-project).

Deze case study beschrijft een gedeelte van een geïntegreerde staalfabriek van SIDMAR in Gent. Het probleem bestaat daarin om voor een gegeven volgorde van producten een rooster te vinden dat aan de beperkingen van de fabriek voldoet. Om dit probleem te benaderen, wordt onderzocht of met behulp van getimede automaten een model gegeven kan worden zodanig dat een bereikbaarheidsanalyse een geldig rooster op kan leveren. Voor modellering en analyse kan in dit geval gebruik gemaakt worden van tools voor getimede automaten zoals Uppaal. Aan deze aanpak kleven echter twee nadelen. Modellen zijn dikwijls zo groot dat de bereikbaarheidsanalyse geen resultaat oplevert. Wordt echter een geldig schedule gevonden wordt is dit vaak verre van optimaal. Onderzoek naar Branch-and-Bound-achtige methoden, moet aangeven hoe deze problemen op kunnen lossen. Deze helpen om het zoeken naar een bereikbare eindtoestand te sturen, en de te doorzoeken toestandsruimte te verkleinen.

De eerste resultaten en modellen voor Case Study 5 werden gepresenteerd tijden een VHS-meeting in Grenoble in Januari. Naar aanleiding hiervan vond van medio Maart een werkbezoek bij Brics in Aalborg plaats. Tijdens de eerstvolgende meeting in Gent werden de resultaten hiervan gepresenteerd.

Samen met Peter Niebert van het Verimag in Grenoble werd aan een taal voor beschrijving van industriële schedulingproblemen. In dit kader vond een werkbezoek in Grenoble plaats.

In het vervolg werd onderzoek gedaan in hoeverre Branch-and-Bound-achtige methoden in bestaande tools zoals Uppaal opgenomen kunnen worden. Een implementatie van de ontwikkelde algoritmes zal in het begin van 2000 plaatsvinden.

Ansgar Fehnker heeft verder assistentie verleent met het organiseren van de internationale workshop Hybrid Systems 98 in Berg en Dal, Nijmegen.