Decisional Architecture theme covers researches in the following area:

Validation and Verification in Robotics

Integration of Decision in Robotics

Validation and Verification in Robotics

The long-term objective of this research is to offer the possibility of validating and verifying all the software that makes up an autonomous system, from the lowest level of control loops to deliberative functions.

This work greatly benefit from our collaboration with the VERTICS team whose tools and approaches (Fiacre, TINA, Hippo) are well suited to the problem we want to address.

The approach we pursue can be caracterized along the following original lines and features:

• The current approach encompasses functional level components and the acting level skills.
• These functional components are fully specified with GenoM by robot programmers (not expert in formal models) and the component regular implementation is already automatically synthesized from these specifications.
• The skills are specified with a new langage proskill which combines the skill langage described in [Albore et al., 2023, Fig. 7] (for basic skill, i.e. the one calling component services) and the procedural langage deployed in OpenPRS [Ingrand et al., 1996] (for composite skills combining the basic and the composite ones).
• The formal models in Fiacre are automatically synthesized from these specifications (both for the components and the skills) and, for the component, it has a consistent semantics with the one of the component regular implementation.
• The synthesized formal models in Fiacre can then be used both offline (with Tina) for verification with model-checking tools and online (with Hippo) for runtime verification and properties enforcement.

The most recent results are:

• A complete and trustfull Fiacre/H-Fiacre model of any GenoM components. The model
  is so close to the regular component implementation that we cannot distinguish them while running on our robots.
• An Hippo engine able to completely run any GenoM components H-Fiacre model,
• Complex experiments where the Hippo engine execute the full model and runs onboard a drone embedded computer and control it at 10 kHz.
• Proskill, a new skills langage which allows us to control multiple component with complex programs (including test, parallelism, loop) while taking into account the preconditions, effects, invariants on skills and modeling external events as well as state variables transitions.

Numerous challenges remain to be met:

• the V&V of learned models, whether used for perception or decision making, whose sensitivity to minor changes in input results in false positives that prohibit their use in critical systems.
• the integration, coherence and interoperability of the various formal models used in the different system components.
• the integration of human beings into the models and into the verification process, whether they are team members, assistants, users or just present in the environment, etc.
• the systematic deployment of safety monitors based on formal operational models, which would remain the ultimate safeguard when off-line methods have shown their limits.

Publications:

• A formal toolchain for offline and run-time verification of robotic systems Silvano Dal Zilio, Pierre-Emmanuel Hladik, Félix Ingrand, Anthony Mallet Robotics and Autonomous Systems, 2023, 159, pp.104301. ⟨10.1016/j.robot.2022.104301⟩
• 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, 2021, 181, pp.111033. ⟨10.1016/j.jss.2021.111033⟩

Integration of Decision in Robotics