Proving Simulink Block Diagrams Correct via Refinement

Simulink is a well-known block diagram-based tool for modular design and multidomain simulation of Cyber-Physical Systems (CPS). However, the simulation by Simulink cannot completely cover the state space or behavior of a target system, which would not ensure the correctness of the developed block diagrams in Simulink. In this work, we present a contract-based method, which supports compositional reasoning and refinement, for proving the correctness of Simulink block diagrams with discrete-time and continuous-time dynamic behavior. We use the assume-guarantee contract as a specification language. The Simulink block diagrams are correct in the sense that if the block diagrams satisfy the formal specifications of the system being modeled. To prove the correctness of a block diagram, we first define semantics for Simulink block diagrams. We study three composition operators, i.e., serial, parallel, and algebraic loop-free feedback with multistep delays. We present a satisfaction relation between the block diagram and contract and present a refinement relation between the contracts. We prove that if the Simulink block diagram satisfies the composition contract and the composition contract refines the system specifications, the block diagram is correct relative to the system specifications. Furthermore, we demonstrate the effectiveness of our method via a real-world case study originating from the control system of a reservoir. Our method can also provide an idea to verify whether the designed CPS is planted with a logic bomb by attackers.