Article (Scientific journals)
Specification Patterns for Robotic Missions
MENGHI, Claudio; Tsigkanos, Christos; Pelliccione, Pelliccione et al.
2019In IEEE Transactions on Software Engineering
Peer reviewed


Full Text
Author postprint (15.06 MB)

All documents in ORBilu are protected by a user license.

Send to


Keywords :
Software; Service robots; Natural languages; Software engineering; Tools; Task analysis
Abstract :
[en] Mobile and general-purpose robots increasingly support our everyday life, requiring dependable robotics control software. Creating such software mainly amounts to implementing their 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 the behavior a robot should have. 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 of which detailing 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 realistic textual 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 we defined with two well-known industrial partners developing human-size robots. We validated our patterns' correctness with simulators and two different types of real robots.
Research center :
Interdisciplinary Centre for Security, Reliability and Trust (SnT) > Software Verification and Validation Lab (SVV Lab)
Disciplines :
Computer science
Author, co-author :
MENGHI, Claudio ;  University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT)
Tsigkanos, Christos;  Technische Universität Wien = Vienna University of Technology - TU Vienna
Pelliccione, Pelliccione;  Chalmers University of Technology and University of Gothenburg, Sweden and University of L’Aquila, Italy
Ghezzi, Carlo;  Politecnico di Milano, Italy
Berger, Thorsten;  Chalmers University of Technology and University of Gothenburg, Sweden
External co-authors :
Language :
Title :
Specification Patterns for Robotic Missions
Publication date :
04 October 2019
Journal title :
IEEE Transactions on Software Engineering
Publisher :
Institute of Electrical and Electronics Engineers, New York, United States - New York
Peer reviewed :
Peer reviewed
Focus Area :
Security, Reliability and Trust
European Projects :
H2020 - 694277 - TUNE - Testing the Untestable: Model Testing of Complex Software-Intensive Systems
Funders :
CE - Commission Européenne [BE]
Available on ORBilu :
since 14 January 2020


Number of views
135 (24 by Unilu)
Number of downloads
258 (10 by Unilu)

Scopus citations®
Scopus citations®
without self-citations
WoS citations


Similar publications

Contact ORBilu