On the mutual dependency of safety controllers and procedural controllers

Formal methods for discrete event controller synthesis and verification are often based on abstract models which neglect details of the implementation of the controller. In practice, however, implementational issues play a very important role. We show by means of formal models of plant, safety controller, and procedural controller that preserve implementational details that the way the controllers are implemented has effects on the closed-loop behavior. As a consequence, we think that implementational details must be included in formal frameworks for controller synthesis or verification