Model Checking Real-Time Properties on the Functional Layer of Autonomous Robots

Mohammed Foughali, Bernard Berthomieu, Silvano Dal Zilio, Félix Ingrand, Anthony Mallet
In ICFEM 2016 — 18th International Conference on Formal Engineering Methods, nov 2016.

 PDF  DOI〈10.1007/978-3-319-47846-3_24〉  HAL-01346080

Abstract

#

Software is an essential part of robotic systems. As robots and autonomous systems are more and more deployed in human environments, we need to use elaborate validation and verification techniques in order to gain a higher level of trust in our systems. This motivates our determination to apply formal verification methods to robotics software. In this paper, we describe our results obtained using model-checking on the functional layer of an autonomous robot. We implement an automatic translation from GenoM, a robotics model-based software engineering framework, to the formal specification language Fiacre. This translation takes into account the semantics of the robotics middleware. TINA, our model-checking toolbox, can be used on the synthesized models to prove real-time properties of the functional modules implementation on the robot. We illustrate our approach using a realistic autonomous navigation example.

Citation

#

@InProceedings{DalzilioS:icfem2016robots,
   author    = {Foughali, Mohammed and Berthomieu, Bernard and {Dal Zilio}, Silvano and Ingrand, Félix and Mallet, Anthony},
   title     = {{Model Checking Real-Time Properties on the Functional Layer of Autonomous Robots}},
   booktitle = {ICFEM 2016 -- 18th International Conference on Formal Engineering Methods},
   series    = {Lecture Notes in Computer Science},
   volume    = {10009},
   publisher = {Springer-Verlag},
   doi = {10.1007/978-3-319-47846-3_24},
   pages     = {383--399},
   month     = nov, 
   year      = 2016
}