Hierarchical Multi-Formalism Proofs of Cyber-Physical Systems

Abstract

To manage design complexity and provide verification tractability, models of complex cyber-physical systems are typically hierarchically organized into multiple abstraction layers. High-level analysis explores interactions of the system with its physical environment, while embedded software is developed separately based on derived requirements. This separation of lowlevel and high-level analysis also gives hope to scalability, because we are able to use tools that are appropriate for each level. When attempting to perform compositional reasoning in such an environment, care must be taken to ensure that results from one tool can be used in another to avoid errors due to “mismatches� in the semantics of the underlying formalisms. This paper proposes a formal approach for linking high-level continuous time models and lower-level discrete time models. Specifically, we lift a discrete-time controller specified using synchronous observer properties into continuous time for proof using timed automata (UPPAAL). To define semantic compatibility between the models, we propose a direct semantics for a network of timed automata with a discrete-time component called Contract- Extended Network of Timed Automata (CENTA) and examine semantic issues involving timing and events with the combination. We then propose a translation of the discrete-time controller into a timed automata state machine and show the equivalence of the translation with the CENTA formulation. We demonstrate the usefulness of the approach by proving that a complex medical infusion pump controller is safe with respect to a continuous time clinical scenario.