Specification and Verification of Controlled Systems

. We propose a conceptual framework to support specification, design and verification of programs controlling physical systems. We introduce a computational model that represents the controller capabilities and distinguishes between synchronous and phase transitions. A graphical system description language is proposed that we believe is readily accessible to control engineers. We formalize the notion of control strategy in controller design. 1 Introduction We present a conceptual framework to reason about controlled systems. We define a controlled system to be a plant consisting of both discrete and continuous components, subject to disturbances from the environment, and controlled by a digital control program, also called the controller (see Figure 1). Controller Plant - oe ? Disturbances (Environment) Fig. 1. Controlled system ? This paper appeared in the Proceedings of the Third International Symposium on Formal Techniques in Real-time and Fault-tolerant Systems, Lecture Notes i..