A graphical environment to express the semantics of control systems
For control system engineers, this work provides a conceptual framework to integrate formal verification into graphical design environments, but it is incremental as it extends existing annotation capabilities without presenting a working implementation or empirical results.
The paper proposes extensions to Simulink-like environments to include formal control system stability and performance properties and their proofs, enabling graphical annotation and translation to verification languages like Lustre or C.
We present the concept of a unified graphical environment for expressing the semantics of control systems. The graphical control system design environment in Simulink already allows engineers to insert a variety of assertions aimed the verification and validation of the control software. We propose extensions to a Simulink-like environment's annotation capabilities to include formal control system stability, performance properties and their proofs. We provide a conceptual description of a tool, that takes in a Simulink-like diagram of the control system as the input, and generates a graphically annotated control system diagram as the output. The annotations can either be inserted by the user or generated automatically by a third party control analysis software such as IQC$β$ or $μ$-tool. We finally describe how the graphical representation of the system and its properties can be translated to annotated programs in a programming language used in verification and validation such as Lustre or C.