ANALYSIS OF SAFETY PROPERTIES IN THE SYNTHESIS OF DISCRETE-EVENT CONTROLLERS

Abstract An “ad-hoc” formal framework is proposed for the analysis of three types of safety specifications describing the conditional execution of finite sequences of controlled events. The notion of a specification set free of errors and redundancies is introduced as a minimal set of consistent specifications as well as procedures to establish it. The satisfiability verification of the specifications by the closed-loop behavior model is also discussed. The use and advantages of the framework are illustrated with the synthesis of a class of discrete-event controller, termed procedural controller, for the operation of an industrial batch chemical reactor. Conflicts on the specification set were easily identified and corrected, reducing the synthesis effort. Satisfiability verification of the specifications by the closed-loop behavior establishes to what extent the controller fulfills the specifications.