An integrated state- and event-based framework for verifying liveness in supervised systems

J. Markovski, M.A. Reniers

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    4 Citations (Scopus)

    Abstract

    Supervisory control theory deals with synthesis of discrete-event supervisory controllers that ensure safe (and nonblocking) behavior of the supervised system. However, the synthesized supervisor comes with no guarantees regarding desired functionality beyond nonblocking behavior. This typically occurs when the control requirements imposed on the system are too strict, or the model of the system needs to be refined. To provide concise and useful feedback to the modeler, we propose an integrated state- and event-based systems engineering framework using state-of-the-art tools: Supremica for supervisor synthesis and mCRL2 for verification. Stating properties in terms of both states and transitions is important in the domain of supervisor synthesis as many control and liveness requirements involve combined state- and event-based specifications. However, many of the available verification tools either focus on state-based or event-based properties. We seek to remedy this situation by providing verification patterns that typically occur in industrial application of supervisory control. We illustrate the framework by revisiting an industrial case study of coordinating maintenance procedures of a high-tech Oce printer, for which we verify the functionality of the solution.
    Original languageEnglish
    Title of host publicationProceedings of the 2010 11th International Conference on Control Automation Robotics & Vision (ICARCV), 5-7 December 2012, Guangzhou, China
    Place of PublicationPiscataway
    PublisherInstitute of Electrical and Electronics Engineers
    Pages246-251
    ISBN (Print)978-1-4673-1870-9
    DOIs
    Publication statusPublished - 2012
    Event12th International Conference on Control, Automation, Robotics and Vision (ICARCV 2012) - Guangzhou, China
    Duration: 5 Dec 20127 Dec 2012
    Conference number: 12

    Conference

    Conference12th International Conference on Control, Automation, Robotics and Vision (ICARCV 2012)
    Abbreviated titleICARCV 2012
    Country/TerritoryChina
    CityGuangzhou
    Period5/12/127/12/12

    Fingerprint

    Dive into the research topics of 'An integrated state- and event-based framework for verifying liveness in supervised systems'. Together they form a unique fingerprint.

    Cite this