Supervisory control theory toegepast op pretparkvoertuigen

De hightechindustrie staat voor de uitdaging om de functionaliteit en kwaliteit van een product te verhogen en tegelijkertijd de doorlooptijd en de kosten van het ontwikkeltraject te verlagen. Nieuwe systeemontwikkelprocessen kunnen hierbij helpen. In dit artikel willen we laten zien hoe de zogeheten supervisory control theory (SCT) van Murray Wonham and Peter Ramadge uit 1984 kan bijdragen aan de ontwikkeling van besturingssystemen en hoe we supervisorsynthese kunnen integreren in een systeemontwikkelproces.

Supervisory control synthesis gaat uit van een te besturen systeem (plant) P en een supervisor S (Figuur 1). Eerst leggen we de requirements R vast van het systeem, op basis waarvan we een systeemdesign D definiëren en een opdeling in de te besturen plant en de supervisor. Vervolgens specificeren we de eisen aan de supervisor RS en aan de te besturen plant RP. De eerste modelleren we formeel; met de tweede maken we een ontwerp DP en een of meer plantmodellen. Uit het model RS en een plantmodel met discrete acties leiden we ten slotte de supervisor af, de synthese. De plantmodellen kunnen we ook in simulatie gebruiken om het gedrag te analyseren van de plant die wordt bestuurd door de supervisor. Als we modellen hebben van alle systeemcomponenten, kunnen we verschillende analysetechnieken inzetten om het geheel te testen in een vroeg stadium van het ontwikkeltraject.

In systeemontwikkeling op basis van synthese kunnen we eigenschappen die in traditionele en modelgebaseerde ontwikkeling pas achteraf worden gecheckt, gebruiken als input voor het ontwerp van een component die correct is door constructie. Als gevolg hiervan hoeven we het design en de implementatie niet te testen op de gestelde eisen. We kunnen de verificatie dus overslaan. Dit verandert het ontwikkeltraject: we hoeven de fouten niet meer uit het ontwerp en de implementatie te halen, maar in plaats daarvan uit de gestelde eisen.

Figuur 2 toont een schematisch overzicht van het besturingsgedeelte van een hightech systeem. Onderaan staat het te besturen systeem afgebeeld met de fysieke hardwarecomponenten. Hierop zitten sensoren en actuatoren gemonteerd die de plaats en toestand van de componenten waarnemen en daar invloed op uitoefenen. Regelaars verwerken de sensorsignalen en besturen de actuatoren, zodat de bijbehorende component de gewenste positie op de gewenste manier bereikt. Dit is het niveau van de resource control, het regelgedeelte. Daarboven staat de supervisory control, het coördinatiegedeelte. Dit deel coördineert de verschillende componenten en realiseert zo de gewenste systeemfunctionaliteit.

In de context van SCT modelleren we een te besturen systeem middels een of meerdere zogeheten eindige automaten, bestaande uit toestanden met overgangen daartussen, en stellen we eisen op die eigenschappen specificeren waaraan het bestuurde systeem moet voldoen. Acties verdelen we aan de ene kant in controleerbare en oncontroleerbare acties, en aan de andere kant in observeerbare en onobserveerbare acties. Het hart van de theorie is het synthetiseren (het afleiden) van een supervisor, die alleen controleerbare acties kan verbieden, die nieuwe mogelijke acties kan bepalen na nieuwe observaties en die altijd garandeert dat het bestuurde systeem een goede eindtoestand kan bereiken, in welke toestand het zich ook bevindt.

In het algemeen zijn er twee besturingsstrategieën te onderscheiden: toestandsgebaseerde en actiegebaseerde regeling. Bij de eerste heeft de supervisor alleen informatie over toestanden ter beschikking en bij de tweede alleen informatie over series observeerbare acties. Op basis van observaties bepaalt de supervisor welke acties kunnen worden uitgevoerd vóór nieuwe observaties worden gedaan. Wij passen hier beide strategieën toe.

Als het systeem niet te ingewikkeld is, kunnen we een gecentraliseerde supervisor synthetiseren. Helaas hebben we bij deze aanpak last van het fenomeen van de toestandsruimte-explosie (state space explosion), een exponentiële toename van het aantal toestanden. Deze computationele complexiteit noopt tot meer geavanceerde synthesetechnieken zoals de symbolische berekeningsmethode met toestandsgebaseerde aanpak van Wonham en zijn discipel Chuan Ma of de aanpak met gedistribueerde synthese van onze collega‘s Rong Su, Jan van Schuppen en Koos Rooda. In onze casestudy passen we verschillende synthesetechnieken toe en kijken we wat het beste werkt voor complexe systemen en herconfigureerbaarheid.

Logische specificaties

Onderwerp van deze studie is een echt systeem: de besturing die NBG Industrial Automation uit Nederweert heeft ontwikkeld voor de Multimover van plaatsgenoot ETF Ride Systems. Dit is een automatisch geleid voertuig dat een in de vloer gelegde elektriciteitskabel kan volgen. Deze kabel produceert een magnetisch veld dat het wagentje kan oppikken met sensoren. Er zijn ook vloercodes die het kan inlezen met een metaaldetector en die extra informatie geven over de te volgen route, zoals het begin van een scèneprogramma of een wissel, kruising of doodlopend spoor. Het scèneprogramma bepaalt wanneer het voertuig moet bewegen, met welke snelheid, wanneer het moet stoppen, ronddraaien, muziek moet laten horen en in welke richting het moet gaan (bijvoorbeeld bij een kruising).

Een operator activeert het karretje in een attractie en bestuurt het bij het instappen en uitstappen van de passagiers. De wagen krijgt daarbij boodschappen van de Ride Control, die alle voertuigen coördineert en draadloos de start- en stopcommando‘s stuurt. De Multimovers kunnen niet communiceren met elkaar. Omdat passagiersveiligheid heel belangrijk is, zijn er verschillende sensoren om botsingen te voorkomen. Allereerst zitten er naderingssensoren in het voertuig om fysiek contact met andere objecten te vermijden. Er zijn twee types: langeafstandssensoren die obstakels kunnen waarnemen op een afstand van ongeveer zes meter en korteafstandssensoren met een bereik van ongeveer een meter. Daarnaast zit er een bumperschakelaar op het karretje die fysiek contact met andere objecten kan waarnemen.

De belangrijkste eis is dus veiligheid. De supervisor moet ervoor zorgen dat de Multimover niet botst met andere voertuigen of obstakels. Zo nodig moet hij de snelheid aanpassen of het voertuig stoppen. Als zich dan toch een botsing voordoet, moet hij het wagentje onmiddellijk stil- en de motor uitzetten. Dit moet ook gebeuren als de accu leeg is of als er een motorstoring of een andere fout optreedt. Een lampje moet aangaan als een noodstop is uitgevoerd, waarna de operator het probleem moet oplossen.

De plant in deze casestudy is een actiegebaseerde abstractie van het werkelijke gedrag van de fysieke componenten en hun regelaars, zoals getoond in Figuur 3. Pijlen representeren de informatievoorziening tussen de componenten, de resource control (RC) en de supervisor. Elke component samen met zijn regelaar hebben we gemodelleerd met één automaat. Automaten hebben toestanden en overgangen daartussen, gelabeld met acties. Toestanden representeren alle relevante componenttoestanden, zoals aan, uit, leeg of actief. Controleerbare acties zijn relevante discrete commando‘s aan de component, zoals aan- of uitzetten. De supervisor kan deze wel of niet toestaan. Oncontroleerbare acties zijn boodschappen van de component aan de supervisor, zoals een foutmelding of sensorwaarde. Deze kan de supervisor niet tegenhouden.

Het plantmodel hebben we gemaakt onder de aanname dat de werking van de resourcecontrollers correct is. Deze aanname is redelijk omdat zij deel uitmaken van de bestaande implementatie en uitvoerig zijn getest. Dit betekent dat we ervan kunnen uitgaan dat elke opdracht aan de resourcecontrollers correct wordt uitgevoerd. Een andere aanname is dat de communicatie tussen de plant en zijn supervisor voldoende snel is. Als een actie is uitgevoerd in de plant, bijvoorbeeld het indrukken van een knop, heeft de supervisor dit onmiddellijk door. Verderop zullen we aannemelijk maken dat dit ook het geval is voor onze prototype implementatie.

Het actiegebaseerde raamwerk gebruikt automaten om plant- en eismodellen in te vatten. Soms is het echter makkelijker of intuïtiever eisen te specificeren met expressies over toestanden. Deze geven een veel compactere beschrijving, waar de automaten waarop SCT is gebaseerd alle mogelijke gedragingen op een omslachtige manier uitdrukken. Bovendien hebben systeemeisen vaak de vorm van condities over toestanden. Het toestandsgebaseerde raamwerk biedt beide mogelijkheden om het gewenste gedrag te specificeren. Op de TUE hebben we bovendien een uitbreiding hierop ontwikkeld om toestandsgebaseerde expressies automatisch te genereren uit logische specificaties, die weer op een natuurlijke manier volgen uit informele en intuïtieve eisen. Zo zijn deze requirements eenvoudig om te zetten in een formaat dat past in het toestandsgebaseerde raamwerk.

Communicatieprobleem

De Multimover is zo complex (Tabel 1) dat het onmogelijk is om met een actiegebaseerde werkwijze één gecentraliseerde supervisor te maken. Daarom hebben we een gecentraliseerde toestandsgebaseerde supervisor afgeleid met de aanpak van Ma en Wonham en twee gedistribueerde actiegebaseerde supervisors met de methode van Su, Van Schuppen en Rooda. Uit ons experiment blijkt dat deze combinatie goed werkt bij problemen van deze omvang. Met een geautomatiseerde conversie hebben we vervolgens de eisen gemodelleerd. Deze conversie formaliseert de requirements door ze om te zetten in logische expressies of automaten, waarna er een gedistribueerde supervisor uit is af te leiden.

De gesynthetiseerde supervisors hebben we geanalyseerd om te controleren of de modellen van het bestuurde systeem kloppen met het gewenste gedrag. Daarbij hebben we een simulator gebruikt die door de toestandsruimte kan stappen, zodat we kunnen nagaan of de juiste transities kunnen optreden in de juiste toestanden. Hiermee kunnen we ook zeldzame situaties simuleren. De gebruikte simulator hoort bij de toolset die we bij de TUE-faculteit Werktuigbouwkunde hebben ontwikkeld.

Een supervisor in SCT is een passieve component die plantacties bijhoudt en het plantgedrag inperkt door controleerbare acties te verbieden. In de praktijk moeten deze acties vaak worden geïnitieerd – machines hebben een startcommando nodig om te beginnen. Daarom hebben we een besturing nodig die niet alleen controleerbare acties verbiedt, maar ze ook kan initiëren. Een ander punt is dat we aannemen dat er geen communicatievertraging is tussen plant en supervisor. In modellen hebben we synchrone communicatie, maar in echte systemen vaak asynchrone. Daarom is een supervisor niet direct een controller, maar eerder een component die aangeeft welke acties zijn toegestaan in elke planttoestand.

Een supervisory controller heeft twee taken: hij moet de toestand van de plant bijhouden zodat die de juiste terugkoppeling krijgt en hij moet de juiste stuuracties doorgeven aan de plant, uitgaande van diens toestand (Figuur 4). Als zich in de plant een actie voordoet, bijvoorbeeld het indrukken van een knop of de activatie van een sensor, wordt dit gemeld zodat de supervisor de huidige toestand kan updaten. Hij geeft dan de nieuwe toestand. Alleen oncontroleerbare acties worden gemeld, de supervisory controller initieert zelf de controleerbare acties. Als hij de toestand heeft geüpdatet, moet hij een juiste stuuractie doorgeven aan de plant, bijvoorbeeld om een lampje aan of een motor uit te zetten. Is de juiste stuuractie gevonden, dan wordt die uitgevoerd en krijgt de toestand in de supervisor weer een update.

In de implementatie zou mogelijk een communicatieprobleem kunnen optreden. Stel, de besturing kan een stuuractie naar de plant zenden, maar ondertussen is diens toestand veranderd, waardoor de actie is gebaseerd op een oude situatie. Dit kan gebeuren omdat de communicatie tussen plant en supervisor niet synchroon is. Bij ons experiment hebben we uitgaande van de gesynthetiseerde supervisor een prototype supervisory controller geïmplementeerd in de bestaande besturingssoftware van de Multimover. Die implementatie hebben we eerst gesimuleerd in de testopstelling en daarna in het echte voertuig. Het communicatieprobleem kwam niet voor. Dit komt doordat de supervisor snel genoeg reageert op toestandsveranderingen van de plant: in de toestandsgebaseerde supervisor is de reactietijd 80 ms en in de actiegebaseerde supervisor 20 ms. Dit is voldoende snel voor de Multimover. Onze prototype implementatie maakt dus de aannames over asynchroniteit en het instantaan optreden van acties waar.

De resultaten van de casestudy laten zien dat de synthesetechnieken effectief zijn, in het bijzonder als eisen of componenten van de plant veranderen of als we het systeem moeten herconfigureren. Dit is gestoeld op de volgende observatie. In het huidige ontwikkelproces zijn ongeveer twee dagen nodig om het besturingssysteem aan te passen als het aantal naderingssensoren wordt uitgebreid. Het synthesegebaseerde proces beschreven in dit artikel heeft ongeveer vier uur nodig voor dezelfde verandering.

Beter begrip

Formele modellen spelen een sleutelrol in een systeemontwikkelproces met synthese. Ze geven een gestructureerde en systematische aanpak om het gedrag van componenten en systemen te specificeren. Ze zijn consistenter en minder ambigu dan documenten. De formele semantiek definieert precies wat de modellen betekenen. Het gebruik van formele modellen al vroeg in het systeemontwikkelproces dwingt de ontwerper om alle aspecten van het systeem helder neer te zetten. Helderheid draagt bij aan een goed ontwerp en correcte besturingssoftware. Het modelleren van systemen en systeemeisen met eindige automaten of logische expressies is intuïtief. Het kost wel tijd om modelleervaardigheden te ontwikkelen.

De automatische supervisorsynthese verandert het softwareontwikkelproces van het ontwerpen en debuggen van besturingscode naar het ontwerpen en debuggen van eisen, mits de plantmodellen correct zijn. Omdat we de eisen formeel hebben gemodelleerd, hoeven we het model van de supervisor niet te testen tegen de eisen; het is correct door constructie. Zodoende kunnen we ons beperken tot validatie van het systeem en is verificatie van het softwareontwerp niet nodig. En als de eisen veranderen door klantvragen, hoeven we het ontwerp niet meer handmatig aan te passen met alle fouten en inconsistenties van dien. Met de synthesegebaseerde aanpak hoeven we alleen de modellen van de plant of van de eisen te wijzigen, waarna we een nieuwe supervisor kunnen synthetiseren. Dit houdt in dat het systeem kan evolueren, veranderingen aankan.

Bovendien kunnen we gesynthetiseerde supervisors meteen simuleren, wat een snelle terugkoppeling in het ontwikkelproces mogelijk maakt. Het gebruik van modellen en de bijbehorende analysetechnieken als simulatie en formele verificatie laat toe om fouten in een vroeg stadium van het systeemontwikkelproces te ontdekken. Daardoor kunnen we besparen op het ontwikkelen van dure prototypes. Omdat we het gewenste gedrag hebben vastgelegd in modellen en niet in code, hebben we een beter begrip van de besturingssoftware, met als gevolg dat de validatie ten opzichte van de oorspronkelijke informele specificaties gemakkelijker wordt.