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

Autor: Pierre-Emmanuel Hladik, Reyyan Tekin, Silvano Dal Zilio, Félix Ingrand
Přispěvatelé: Équipe Verification de Systèmes Temporisés Critiques (LAAS-VERTICS), Laboratoire d'analyse et d'architecture des systèmes (LAAS), Université Toulouse 1 Capitole (UT1), Université Fédérale Toulouse Midi-Pyrénées-Université Fédérale Toulouse Midi-Pyrénées-Institut National des Sciences Appliquées - Toulouse (INSA Toulouse), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université Toulouse - Jean Jaurès (UT2J)-Université Toulouse III - Paul Sabatier (UT3), Université Fédérale Toulouse Midi-Pyrénées-Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique (Toulouse) (Toulouse INP), Université Fédérale Toulouse Midi-Pyrénées-Université Toulouse 1 Capitole (UT1), Université Fédérale Toulouse Midi-Pyrénées, Équipe Robotique et InteractionS (LAAS-RIS), ANR-19-P3IA-0004,ANITI,Artificial and Natural Intelligence Toulouse Institute(2019), European Project: 825619,AI4EU, Université Toulouse 1 Capitole (UT1)-Institut National des Sciences Appliquées - Toulouse (INSA Toulouse), Université Fédérale Toulouse Midi-Pyrénées-Université Fédérale Toulouse Midi-Pyrénées-Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique (Toulouse) (Toulouse INP), Université Fédérale Toulouse Midi-Pyrénées-Université Toulouse 1 Capitole (UT1)-Institut National des Sciences Appliquées - Toulouse (INSA Toulouse), Université Toulouse Capitole (UT Capitole), Université de Toulouse (UT)-Université de Toulouse (UT)-Institut National des Sciences Appliquées - Toulouse (INSA Toulouse), Institut National des Sciences Appliquées (INSA)-Université de Toulouse (UT)-Institut National des Sciences Appliquées (INSA)-Université Toulouse - Jean Jaurès (UT2J), Université de Toulouse (UT)-Université Toulouse III - Paul Sabatier (UT3), Université de Toulouse (UT)-Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique (Toulouse) (Toulouse INP), Université de Toulouse (UT)-Université Toulouse Capitole (UT Capitole), Université de Toulouse (UT), Université Toulouse - Jean Jaurès (UT2J)-Université Toulouse 1 Capitole (UT1), Université Fédérale Toulouse Midi-Pyrénées-Université Fédérale Toulouse Midi-Pyrénées-Centre National de la Recherche Scientifique (CNRS)-Université Toulouse III - Paul Sabatier (UT3), Université Fédérale Toulouse Midi-Pyrénées-Institut National des Sciences Appliquées - Toulouse (INSA Toulouse), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Institut National Polytechnique (Toulouse) (Toulouse INP), Université Fédérale Toulouse Midi-Pyrénées-Université Toulouse - Jean Jaurès (UT2J)-Université Toulouse 1 Capitole (UT1), ANR-19-P3IA-0004 ,ANITI,Artificial and Natural Intelligence Toulouse Institute - Institut 3iA(2019)
Jazyk: angličtina
Rok vydání: 2021
Předmět:
verifiable implementation
Modeling language
Computer science
formal toolchain
02 engineering and technology
[INFO.INFO-SE]Computer Science [cs]/Software Engineering [cs.SE]
computer.software_genre
Toolchain
[INFO.INFO-FL]Computer Science [cs]/Formal Languages and Automata Theory [cs.FL]
0502 economics and business
0202 electrical engineering
electronic engineering
information engineering
[INFO.INFO-RB]Computer Science [cs]/Robotics [cs.RO]
Formal verification
[INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL]
Programming language
05 social sciences
020207 software engineering
computer.file_format
Specification language
robotic case study
Software framework
Hardware and Architecture
Executable
Compiler
computer
050203 business & management
Software
Information Systems
Semantic gap
Zdroj: Journal of Systems and Software
Journal of Systems and Software, Elsevier, In press
Journal of Systems and Software, 2021, 181, pp.111033. ⟨10.1016/j.jss.2021.111033⟩
Journal of Systems and Software, Elsevier, 2021, 181, pp.111033. ⟨10.1016/j.jss.2021.111033⟩
ISSN: 0164-1212
DOI: 10.1016/j.jss.2021.111033⟩
Popis: International audience; 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.
Databáze: OpenAIRE
Externí odkaz: