Critical autonomous systems
The stakes for the safety of autonomous systems are high: the deployment of driverless cars and all kinds of advanced robots depends on the solutions that can be provided. The team's work focuses on methods for analyzing such systems.
The TRUST team is particularly interested in verification methods, both pre-deployment (formal verification [1], simulation-based testing [2,3]) and post-deployment (monitoring and control at runtime [4,5]).
A cross-cutting problem with these methods is the choice of formalisms suitable for modeling software layers. Some specification languages already exist, such as the GenoM framework developed by the RIS team in the ROB department for the functional layer, but others have yet to be developed (e.g. skill-based architectures [6]). These languages need to be translated into formalisms that enable properties to be verified at model level, and code to be generated to check these properties at implementation level.
As far as simulation testing is concerned, a major stumbling block is the complexity of the test environments and situations to be recreated, which poses problems of modeling, constrained test generation and selection.
Références
[1] Silvano Dal Zilio, Pierre-Emmanuel Hladik, Félix Ingrand, Anthony Mallet, "A formal toolchain for offline and run-time verification of robotic systems", Robotics and Autonomous Systems, Vol. 159, 2023.
[2] Clément Robert, Thierry Sotiropoulos, Hélène Waeselynck, Jérémie Guiochet, SimonVernhes, "The virtual lands of Oz : testing an agribot in simulation", Empirical Software Engineering, Vol. 25, no. 3, pp. 2025-2054, 2020.
[3] Mohamed El Mostadi, Hélène Waeselynck, Jean-Marc Gabriel, "Virtual Test Scenarios for ADAS : Distance to Real Scenarios Matters!", Proc. IEEE Intelligent Vehicles Symposium (IV 2022), pp. 836-841, 2022.
[4] Mathilde Machin, Jérémie Guiochet, Hélène Waeselynck, Jean-Paul Blanquart, Matthieu Roy, Lola Masson, "SMOF : A Safety Monitoring Framework for Autonomous Systems", IEEE Transactions on Systems, Man, and Cybernetics : Systems, vol. 48, no. 5, pp. 702-715, 2018.
[5] 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", Journal of Systems and Software, vol. 181, 2021.
