Skip to Main content Skip to Navigation
Preprints, Working Papers, ...

Hippo: A Formal-Model Execution Engine to Control and Verify Critical Real-Time Systems

Pierre-Emmanuel Hladik 1 Félix Ingrand 2 Silvano Dal Zilio 1 Reyyan Tekin 1
1 LAAS-VERTICS - Équipe Verification de Systèmes Temporisés Critiques
LAAS - Laboratoire d'analyse et d'architecture des systèmes
2 LAAS-RIS - Équipe Robotique et InteractionS
LAAS - Laboratoire d'analyse et d'architecture des systèmes
Abstract : The design of embedded real-time systems requires specific toolchains to guarantee time constraints and safe behavior. These tools 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 implementation built around a common formalism. Our formalism 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 highlevel 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 obtain a Hippo model from an initial specification of the system based on the robotics programming framework GenoM. We illustrate our approach by describing how the Hippo runtime is used to control this robot, but also how we can use formal verification to check critical properties on this system.
Complete list of metadatas

https://hal.laas.fr/hal-03017661
Contributor : Felix Ingrand <>
Submitted on : Saturday, November 21, 2020 - 10:29:09 AM
Last modification on : Monday, December 14, 2020 - 6:08:14 PM

File

main_hal.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-03017661, version 1

Citation

Pierre-Emmanuel Hladik, Félix Ingrand, Silvano Dal Zilio, Reyyan Tekin. Hippo: A Formal-Model Execution Engine to Control and Verify Critical Real-Time Systems. 2020. ⟨hal-03017661v1⟩

Share

Metrics

Record views

22

Files downloads

3