Verifying Liveness in Supervised Systems Using UPPAAL and mCRL2

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.