Compositional synthesis of supervisors for modular discrete event systems

Startdatum 2010-03-01
Slutdatum Projektet är avslutat: 2013-02-28

Kompositionell syntes av övervakare för modulära händelsediskreta system

Projektet angriper svårigheterna med att effektivt beräkna en logiskt korrekt övervakare för reaktiva system. Arbetet inriktar sig på att formellt matematiskt utforma datoralgoritmer, och bevisa deras korrekthet. Rättframma metoder att beräkna övervakare faller ofta på ett inneboende komplexitetsproblem, kallat tillståndsexplosion, som också gör manuell design av övervakare hanterbar enbart för små system.

Övervakarsyntes är en formell metod för att skapa korrekta styrfunktioner för tillverkningssystem, inbyggda system och liknande reaktiva system. Dessa har gemensamt att de är säkerhetskritiska, och en övervakare är en säkerhetsanordning som garanterar att det övervakade systemet inte bryter mot de givna specifikationerna. Denna logiska korrekthet är avgörande för säkerheten hos de människor som interagerar med sådana system.
 
Forskningen fokuserar på kompositionella, abstraktionsbaserade syntesmetoder, vilka försöker utnyttja systemets inneboende modulära struktur genom att ersätta systemkomponenter med enklare komponenter med likvärdiga syntesegenskaper. Detta görs iterativt tills det ursprungliga syntesproblemet modifierats till ett motsvarande problem av hanterbar storlek. En övervakare syntetiserad för det enklare problemet är garanterat användbar som övervakare också för det – generellt mycket större – ursprungliga problemet.
 
Forskningen utförs i samarbete med professor Robi Malik, University of Waikato, Hamilton, Nya Zeeland.

 

Publicerad: to 09 feb 2017.