Verifying liveness in supervised systems using UPPAAL and mCRL2

J. Markovski, M.A. Reniers

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

    5 Downloads (Pure)


    Supervisory control ensures safe coordination of high-level discrete-event system behavior. Supervisory controllers observe discrete-event system behavior, make a decision on allowed activities, and communicate the control signals to the involved parties. Models of such controllers are automatically synthesized from the formal models of the unsupervised system and the specified safety requirements. Traditionally, the supervisory controllers do not ensure that intended behavior is preserved, but only ensure that undersired behavior is precluded. Recent work suggested that ensuring liveness properties during the synthesis procedure is a costly undertaking. Therefore, we augment state-of-the-art synthesis tools to provide for efficient post-synthesis verification. To this end, we interface a model-based systems engineering framework with the state-based model checker UPPAAL and the event-based tool suite mCRL2. We demonstrate the framework on an industrial case study involving coordination of maintenance procedures of a high-end printer. Based on our experiences, we discuss the advantages and disadvantages of the used tools. A comparison is given of the functionality offered by the tools and the extent to which these are useful in our proposed method.
    Original languageEnglish
    Title of host publicationICT innovations 2012 : secure and intelligent systems
    EditorsS. Markovski, M. Gusev
    ISBN (Print)978-3-642-37168-4
    Publication statusPublished - 2013
    Eventconference; ICTI 2012 -
    Duration: 1 Jan 2013 → …

    Publication series

    NameAdvances in Intelligent Systems and Computing
    ISSN (Print)2194-5357


    Conferenceconference; ICTI 2012
    Period1/01/13 → …
    OtherICTI 2012


    Dive into the research topics of 'Verifying liveness in supervised systems using UPPAAL and mCRL2'. Together they form a unique fingerprint.

    Cite this