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

Pierre-Emmanuel Hladik, Félix Ingrand, Silvano Dal Zilio, Reyyan Tekin
Journal of Systems and Software 181, nov 2021.

Abstract

#

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.

Citation

#

@Article{DalzilioS:jss2021hippo,
   author  = {Hladik, Pierre-Emmanuel and Ingrand, Félix and {Dal Zilio}, Silvano and Tekin, Reyyan},
   title   = {{Hippo: A formal-model execution engine to control and verify critical real-time systems}},
   journal = {Journal of Systems and Software},
    volume  = {181},
   doi = {10.1016/j.jss.2021.111033},
   month   = nov, 
   year    = 2021
}