The relevance of formal verification methods is widely recognized in the computer science and embedded systems community. Recently, such methods have been introduced also within the control community, to help designers in developing control architectures for complex robotics systems. Robotic systems typically mix continuous and discrete behaviors that cannot be modeled faithfully using neither continuous-only nor discrete-only formalisms. The interaction of continuous and discrete dynamics makes the formal treatment of this kind of systems computationally very demanding, and justifies the need of studying new methods and algorithms. In this paper, we outline the current state-of-the-art, and describe some open problems in verification, refinement and implementation of autonomous robotic systems. We motivate the relevance of our analysis by means of an Autonomous Robotic Surgery test case.

Open Problems in Verification and Refinement of Autonomous Robotic Systems

BRESOLIN, Davide;DI GUGLIELMO, Luigi;GERETTI, Luca;MURADORE, Riccardo;FIORINI, Paolo;VILLA, Tiziano
2012

Abstract

The relevance of formal verification methods is widely recognized in the computer science and embedded systems community. Recently, such methods have been introduced also within the control community, to help designers in developing control architectures for complex robotics systems. Robotic systems typically mix continuous and discrete behaviors that cannot be modeled faithfully using neither continuous-only nor discrete-only formalisms. The interaction of continuous and discrete dynamics makes the formal treatment of this kind of systems computationally very demanding, and justifies the need of studying new methods and algorithms. In this paper, we outline the current state-of-the-art, and describe some open problems in verification, refinement and implementation of autonomous robotic systems. We motivate the relevance of our analysis by means of an Autonomous Robotic Surgery test case.
9780769547985
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: http://hdl.handle.net/11562/473694
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 16
  • ???jsp.display-item.citation.isi??? ND
social impact