Mobile and general-purpose robots increasingly support everyday life, requiring dependable robotics control software. Creating such software mainly amounts to implementing complex behaviors known as missions. Recognizing this need, a large number of domain-specific specification languages has been proposed. These, in addition to traditional logical languages, allow the use of formally specified missions for synthesis, verification, simulation or guiding implementation. For instance, the logical language LTL is commonly used by experts to specify missions as an input for planners, which synthesize a robot's required behavior. Unfortunately, domain-specific languages are usually tied to specific robot models, while logical languages such as LTL are difficult to use by non-experts. We present a catalog of 22 mission specification patterns for mobile robots, together with tooling for instantiating, composing, and compiling the patterns to create mission specifications. The patterns provide solutions for recurrent specification problems; each pattern details the usage intent, known uses, relationships to other patterns, and - most importantly - a template mission specification in temporal logic. Our tooling produces specifications expressed in the temporal logics LTL and CTL to be used by planners, simulators or model checkers. The patterns originate from 245 mission requirements extracted from the robotics literature, and they are evaluated upon a total of 441 real-world mission requirements and 1251 mission specifications. Five of these reflect scenarios defined with two well-known industrial partners developing human-size robots. We further validate our patterns' correctness with simulators and two different types of real robots.

(2021). Specification Patterns for Robotic Missions [journal article - articolo]. In IEEE TRANSACTIONS ON SOFTWARE ENGINEERING. Retrieved from https://hdl.handle.net/10446/237150

Specification Patterns for Robotic Missions

Menghi, Claudio;
2021-01-01

Abstract

Mobile and general-purpose robots increasingly support everyday life, requiring dependable robotics control software. Creating such software mainly amounts to implementing complex behaviors known as missions. Recognizing this need, a large number of domain-specific specification languages has been proposed. These, in addition to traditional logical languages, allow the use of formally specified missions for synthesis, verification, simulation or guiding implementation. For instance, the logical language LTL is commonly used by experts to specify missions as an input for planners, which synthesize a robot's required behavior. Unfortunately, domain-specific languages are usually tied to specific robot models, while logical languages such as LTL are difficult to use by non-experts. We present a catalog of 22 mission specification patterns for mobile robots, together with tooling for instantiating, composing, and compiling the patterns to create mission specifications. The patterns provide solutions for recurrent specification problems; each pattern details the usage intent, known uses, relationships to other patterns, and - most importantly - a template mission specification in temporal logic. Our tooling produces specifications expressed in the temporal logics LTL and CTL to be used by planners, simulators or model checkers. The patterns originate from 245 mission requirements extracted from the robotics literature, and they are evaluated upon a total of 441 real-world mission requirements and 1251 mission specifications. Five of these reflect scenarios defined with two well-known industrial partners developing human-size robots. We further validate our patterns' correctness with simulators and two different types of real robots.
articolo
2021
Menghi, Claudio; Tsigkanos, Christos; Pelliccione, Patrizio; Ghezzi, Carlo; Berger, Thorsten
(2021). Specification Patterns for Robotic Missions [journal article - articolo]. In IEEE TRANSACTIONS ON SOFTWARE ENGINEERING. Retrieved from https://hdl.handle.net/10446/237150
File allegato/i alla scheda:
File Dimensione del file Formato  
8859226.pdf

Solo gestori di archivio

Versione: publisher's version - versione editoriale
Licenza: Licenza default Aisberg
Dimensione del file 7.29 MB
Formato Adobe PDF
7.29 MB Adobe PDF   Visualizza/Apri
Pubblicazioni consigliate

Aisberg ©2008 Servizi bibliotecari, Università degli studi di Bergamo | Terms of use/Condizioni di utilizzo

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/10446/237150
Citazioni
  • Scopus 22
  • ???jsp.display-item.citation.isi??? 29
social impact