Mission Specification Patterns for Mobile Robots: Providing Support for Quantitative Properties
With many applications across domains as diverse as logistics, healthcare, and agriculture, service robots are in increasingly high demand. Nevertheless, the designers of these robots often struggle with specifying their tasks in a way that is both human-understandable and sufficiently precise to enable automated verification and planning of robotic missions. Recent research has addressed this problem for the functional aspects of robotic missions through the use of mission specification patterns. These patterns support the definition of robotic missions involving, for instance, the patrolling of a perimeter, the avoidance of unsafe locations within an area, or reacting to specific events. Our article introduces a catalog of QUantitAtive RoboTic mission spEcificaTion patterns (QUARTET) that tackles the complementary and equally important challenge of specifying the reliability, performance, resource usage, and other key quantitative properties of robotic missions. Identified using a methodology that included the analysis of 73 research papers published in 17 leading software engineering and robotics venues between 2014–2021, our 22 QUARTET patterns are defined in a tool-supported domain-specific language. As such, QUARTET enables: (i) the precise definition of quantitative robotic-mission requirements and (ii) the translation of these requirements into probabilistic reward computation tree logic (PRCTL), supporting their formal verification and automated planning of robotic missions. We demonstrate the applicability of QUARTET by showing that it supports the specification of over 95% of the quantitative robotic mission requirements from a systematically selected set of recent research papers, of which 75% can be automatically translated into PRCTL for the purposes of verification through model checking and mission planning.
Wed 17 JulDisplayed time zone: Brasilia, Distrito Federal, Brazil change
11:00 - 12:30 | Formal VerificationDemonstrations / Journal First / Research Papers / Industry Papers at Pitanga Chair(s): Yunja Choi Kyungpook National University | ||
11:00 18mTalk | A Transferability Study of Interpolation-Based Hardware Model Checking to Software Verification Research Papers DOI Media Attached | ||
11:18 9mTalk | CoqPyt: Proof Navigation in Python in the Era of LLMs Demonstrations Pedro Carrott Imperial College London, Nuno Saavedra INESC-ID and IST, University of Lisbon, Kyle Thompson University of California, San Diego, Sorin Lerner University of California at San Diego, João F. Ferreira INESC-ID and IST, University of Lisbon, Emily First University of California, San Diego DOI Pre-print | ||
11:27 9mTalk | How We Built Cedar: A Verification-Guided Approach Industry Papers Craig Disselkoen Amazon Web Services, Aaron Eline Amazon, Shaobo He Amazon Web Services, Kyle Headley Unaffiliated, MIchael Hicks Amazon, Kesha Hietala Amazon Web Services, John Kastner Amazon Web Services, Anwar Mamat University of Maryland, Matt McCutchen , Neha Rungta Amazon Web Services, Bhakti Shah University of St. Andrews, Emina Torlak Amazon Web Services, USA, Andrew Wells Amazon Web Services | ||
11:36 18mTalk | Mission Specification Patterns for Mobile Robots: Providing Support for Quantitative Properties Journal First Claudio Menghi University of Bergamo; McMaster University, Christos Tsigkanos University of Bern, Switzerland, Mehrnoosh Askarpour McMaster University, Patrizio Pelliccione Gran Sasso Science Institute, L'Aquila, Italy, Gricel Vázquez University of York, UK, Radu Calinescu University of York, UK, Sergio García Volvo Cars Corporation, Sweden | ||
11:54 18mTalk | Rigorous Assessment of Model Inference Accuracy using Language Cardinality Journal First Donato Clun Imperial College London, Donghwan Shin University of Sheffield, Antonio Filieri AWS and Imperial College London, Domenico Bianculli University of Luxembourg | ||
12:12 18mTalk | Simulation-based Testing of Simulink Models with Test Sequence and Test Assessment Blocks Journal First Federico Formica McMaster University, Tony Fan McMaster University, Akshay Rajhans Mathworks, Vera Pantelic McMaster University, Mark Lawford McMaster University, Claudio Menghi University of Bergamo; McMaster University |