Synthesizing a Safety Controller for ConnectedSpaces Using Supervisory Control
Baskar Sridharan, Aditya P. Mathur, Kai‐Yuan Cai · Purdue e-Pubs (Purdue University System) · 2002
KaiYuan Cazi Dept. of Automatic Control, Beijing University of Aeronautics and Astronautics, Beijiug 100083, Cbina [email protected] A collection of one or more devices, each described by its Digital Device Manual and reachable over 0. network, is a ConnectedSpace. The behavior of each device is expressed using an extended finite state machine. A set of policies may be enforced on the ConnecledSpace to ensure its safe behavior. Such safety policies are monitored and enforced by a safety controller. We show how a safety controller is synthesized by expressing the ConnectedSpace and the safety policies using the Timed Transition Model (TTM) and the Real-Time Temporal Logic (RTTL), respectively. The resulting behavior of the ConnectedSpace, enforced by the safety controller, is guaranteed to Slltisfy the safety policies. The notions of policy relaxation and safety ranking are novel to this work. The synthesis procedure is modified to incorpomte these two notions. We present an experimental evaluation of the modified synthesis procedure. The experimental results show that the synthesis procedure is scalable with respect to the number of devices, number of policies, and the number of states of the finite state machines.