2011/08/19 by Timothy C. Wang, Wang, Timothy, Romain Jobredeaux +3 · 1 citation
Computer Science · #Embedded Systems Design Techniques #FOS: Computer and information sciences #FOS: Electrical engineering #FOS: Mathematics #Formal Methods in Verification #Optimization and Control (math.OC) #Programming Languages (cs.PL) #Real-Time Systems Scheduling #Systems and Control (eess.SY) #electronic engineering #information engineering
paper · pdf · doi:10.48550/arxiv.1108.4048
openalex publication_date 2011/08/19 · openalex created_date 2025/10/10 · openalex updated_date 2026/08/01
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.