Specification Patterns for Robotic Missions
Mobile robots are increasingly used in complex environments, often for accomplishing tasks by end-users with no knowledge or expertise in mathematics, computer science, or robotics. Providing techniques that support robotic software development is a major software engineering challenge. One of the most prominent software engineering problems in the robotic domain is the definition of the mission the robotic software must accomplish and the translation of this mission into a form that enables automated reasoning. On one hand, missions should be defined with a notation that is sufficiently high-level and user-friendly. On the other hand, to enable automated reasoning, the notation should be unambiguous and provide a formal and precise description of what robots should do in terms of movements and actions. Software engineers typically express robotic missions in natural language (mission requirements) and subsequently translate them into more precise mission specifications. The latter are often expressed in domain-specific languages or temporal logics. Defining robotic missions is generally challenging – as widely recognized in both the software engineering and robotics communities – since mission requirements are often ambiguous, hindering precise and unambiguous specification.
To support engineers in the definition of mission requirements and specifications we proposed a new set of patterns focusing on robot movement, as well as on how robots perform actions within their environment . The set of patterns, in the form of a catalog, has been produced by analyzing 245 natural-language mission requirements systematically retrieved from robotics literature. From these requirements, we identified recurrent mission specification problems and conceived template solutions, organized as patterns. Our patterns provide a vocabulary that supports engineers in defining mission requirements and validated mission specifications for recurrent mission requirements. The usage of our patterns is supported by a tool, namely PsALM (Pattern bAsed Mission specifier ), that allows (i) specifying a mission requirement through a structured English grammar, and (ii)~automatically generating specifications from mission requirements. Our patterns and tool are available online .
We checked the presence of errors in proposed patterns by testing the patterns on a set of 12 randomly generated models representing buildings where a robot is deployed. We considered ten mission requirements (each obtained by combining different patterns), converted the mission requirements into mission specifications and used those to generate robots’ plans. We used a simulator to verify that the plans satisfied the intended mission requirement. We subsequently generated two specifications for each mission requirement obtained by considering different target specification languages. We verified the correspondence among the proposed specifications.
We evaluated the benefits of using our patterns for designing missions. We collected 441 mission requirements in natural language: 436 obtained from robotic development environments used by practitioners, and five defined in collaboration with two well-known robotics companies developing commercial, human-size service robots (BOSCH and PAL Robotics). We showed that most of the mission requirements were ambiguous but expressible using the proposed patterns, and that the usage of our patterns reduces ambiguities. We then evaluated the coverage of mission specifications. We collected 1251 mission specifications from robotic development environments used by practitioners and research publications and show that almost all specifications can be obtained using the proposed patterns (1154 over $251, i.e., ≈ 92%). We also generated specifications for five mission requirements defined in collaboration with the two robotics partners and fed them into an existing planner. The produced plans were correctly executed by real robots, demonstrating the benefits of patterns’ support in real scenarios. Videos are available on our website .
A small fragment of this work has been published as an extended abstract  and a tool-demo paper  where we presented the initial idea and a description of our toolset for early dissemination. Our following paper  presents our work in full extent, explaining the methodology, all patterns along with their formalization, as well as evaluation of the patterns’ correctness and benefit using real-world mission requirements and mission specifications.
 2018. Robotic Patterns. http://roboticpatterns.com/.
 Claudio Menghi, Christos Tsigkanos, Thorsten Berger, and Patrizio Pelliccione. 2019. PsALM: Specification of Dependable Robotic Missions. In Proceedings of the 41st International Conference on Software Engineering: Companion Proceedings (ICSE’19). IEEE Press, 99–102. https://doi.org/10.1109/ICSE-Companion.2019.00048
 C. Menghi, C. Tsigkanos, T. Berger, P. Pelliccione, and C. Ghezzi. 2018. Poster: Property Specification Patterns for Robotic Missions. In 2018 IEEE/ACM 40th International Conference on Software Engineering: Companion (ICSE-Companion). 434–435.
 C. Menghi, C. Tsigkanos, P. Pelliccione, C. Ghezzi, and T. Berger. 2019. Specification Patterns for Robotic Missions. IEEE Transactions on Software Engineering (2019), 1–1. https://doi.org/10.1109/TSE.2019.2945329
Fri 10 JulDisplayed time zone: (UTC) Coordinated Universal Time change
16:05 - 17:05
A24-Testing and Debugging 4Technical Papers / New Ideas and Emerging Results / Journal First / Demonstrations at Silla
Chair(s): Yijun Yu The Open University, UK
|Manifold for Machine Learning AssuranceNIER|
New Ideas and Emerging Results
Taejoon Byun University of Minnesota, Sanjai Rayadurgam University of Minnesota
|On Learning Meaningful Assert Statements for Unit Test CasesTechnical|
Cody Watson Washington and Lee University, Michele Tufano Microsoft, Kevin Moran William & Mary/George Mason University, Gabriele Bavota Università della Svizzera italiana, Denys Poshyvanyk William and MaryPre-print Media Attached
|TRADER: Trace Divergence Analysis and Embedding Regulation for Debugging Recurrent Neural NetworksTechnical|
Guanhong Tao Purdue University, Shiqing Ma Rutgers University, Yingqi Liu Purdue University, USA, Qiuling Xu Purdue University, Xiangyu Zhang Purdue UniversityPre-print
|DeepMutation: A Neural Mutation ToolDemo|
Michele Tufano Microsoft, Jason Kimko William & Mary, Shiya Wang William & Mary, Cody Watson Washington and Lee University, Gabriele Bavota Università della Svizzera italiana, Massimiliano Di Penta University of Sannio, Denys Poshyvanyk William and MaryPre-print
|Specification Patterns for Robotic MissionsJ1|
Claudio Menghi University of Luxembourg, Christos Tsigkanos TU Vienna, Patrizio Pelliccione University of L'Aquila and Chalmers | University of Gothenburg, Carlo Ghezzi Politecnico di Milano, Thorsten Berger Chalmers | University of Gothenburg
|ProXray: Protocol Model Learning and Guided Firmware AnalysisJ1|
Farhaan Fowze University of Florida, Dave (Jing) Tian Purdue University, Grant Hernandez University of Florida, Kevin Butler Univ. Florida, Tuba Yavuz University of Florida
|Visual Sketching: From Image Sketches to CodeNIER|
New Ideas and Emerging Results
Marcelo d'Amorim Federal University of Pernambuco, Rui Abreu Instituto Superior Técnico, U. Lisboa & INESC-ID, Carlos Mello Federal University of PernambucoPre-print Media Attached