Complete validation and verification of the software of an autonomous robot (AR) is out of reach for now. Still, this should not prevent us from trying to verify some properties on components and their integration. There are many approaches to consider for the V&V of AR software, e.g. write high level specifications and derive them in correct implementations, deploy and develop new or modified V&V formalisms to program robotics components, etc. Learned models put aside, most models used in deliberation functions [2] are amenable to formal V&V [1] and we prefer focussing on the functional level V&V challenge. We propose an approach which rely on an existing robotics specification/implementation framework (GenoM) to deploy robotics functional components, to which we harness existing well known formal V&V frameworks (UPPAAL, BIP, FIACRE/TINA). GenoM was originally developed by roboticists and software engineers, who wanted to clearly and precisely specify how a reusable, portable, middleware independent, functional component should be written and implemented. Many complex robotic experiments have been developed and deployed over 20 years using GenoM and it is only recently that its designers realized that the rigorous specification, a clear semantic of the implementation and the template mechanism to synthesize code opens the door to automatic formal model synthesis and formal V&V (offline and online). This bottom up approach, which starts from components implementation, may be more modest than the top down ones which aim at a larger and more global view of the problem. Yet, it gives encouraging results on real implementations on which one can build more complex high level properties to be then verified and validated offline but also with online monitors.
[1] Félix Ingrand. Recent Trends in Formal Validation and Verification of Autonomous Robots Software. IEEE International Conference on Robotic Computing, Feb 2019, Naples, Italy. ⟨hal-01968265⟩ https://hal.laas.fr/hal-01968265
[2] Félix Ingrand, Malik Ghallab. Deliberation for autonomous robots: A survey. Artificial Intelligence, Elsevier, 2017, 247 pp.10-44. ⟨http://www.sciencedirect.com/science/article/pii/S0004370214001350?via%3Dihub⟩. ⟨10.1016/j.artint.2014.11.003⟩. https://hal.laas.fr/hal-01137921
[3] Tesnim Abdellatif, Saddek Bensalem, Jacques Combaz, Lavindra de Silva, Félix Ingrand. Rigorous design of robot software: A formal component-based approach. Robotics and Autonomous Systems, Elsevier, 2012, 60 (12), pp.1563-1578. ⟨10.1016/j.robot.2012.09.005⟩. https://hal.laas.fr/hal-01980036
[4] Mohammed Foughali, Silvano Dal Zilio, Félix Ingrand. On the Semantics of the GenoM3 Framework. Rapport LAAS n° 19036. 2019. https://hal.laas.fr/hal-01992470
