Wed 17 Jul 2024 11:36 - 11:54 at Pitanga - Formal Verification Chair(s): Yunja Choi

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 Jul

Displayed 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
18m
Talk
A Transferability Study of Interpolation-Based Hardware Model Checking to Software VerificationDistinguished Paper Award
Research Papers
Dirk Beyer LMU Munich, Po-Chun Chien LMU Munich, Marek Jankola LMU Munich, Nian-Ze Lee LMU Munich
DOI Media Attached
11:18
9m
Talk
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
9m
Talk
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
18m
Talk
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
18m
Talk
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
18m
Talk
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