HIPPO: A formal-model execution engine to control and verify critical real-time systems

摘要

The design of embedded real-time systems requires specific toolchains to guarantee time constraints and safe behavior. These tools and their artifacts need to be managed in a coherent way all along the design process and need to address timing constraints and execution semantic in a holistic way during the system's modeling, verification, and implementation phases. However, modeling languages used by these tools do not always share a common semantic. This can introduce a dangerous gap between what designers want to express, what is verified and the behavior of the final executable code. In order to address this problem, we propose a new toolchain, called Hippo, that integrates tools for design, verification and execution built around a common formalism. Our approach is based on an extension of the Fiacre specification language with runtime features, such as asynchronous function calls and synchronization with events. We formally define the behavior of these additions and describe a compiler to generate both an executable code and a verifiable model from the same high-level specification. The execution of the resulting code is supported by a dedicated execution engine that guarantees real-time behavior and that reduces the semantic gap between high-level models and executable code. We illustrate our approach with a non-trivial use case: the autonomous navigation of a Segway RMP440 robotic platform. We describe how we derive a Hippo model from an initial specification of the system based on the robotics programming framework G~(en)oM. We also show how to use the HIPPO runtime to control this robot, and how to use formal verification in order to check critical properties on this system.