Scene Flow Specifications: Encoding and Monitoring Rich Temporal Safety Properties of Autonomous Systems
To ensure the safety of autonomous systems, it is imperative for them to abide by their safety properties. The specification of such safety properties is challenging because of the gap between the input sensor space (e.g., pixels, point clouds) and the semantic space over which safety properties are specified (e.g. people, vehicles, road). Recent work utilized scene graphs to overcome portions of that gap, enabling the specification and synthesis of monitors targeting many safe driving properties for autonomous vehicles. However, scene graphs are not rich enough to express the many driving properties that include temporal elements (i.e., when two vehicles enter an intersection at the same time, the vehicle on the left shall yield…), fundamentally limiting the types of specifications that can be monitored. In this work, we characterize the expressiveness required to specify a large body of driving properties, identify property types that cannot be specified with current approaches, which we name scene flow properties, and construct an enhanced domain-specific language that utilizes symbolic entities across time to enable the encoding of the rich temporal properties required for autonomous system safety. In analyzing a set of 114 specifications, we find that our approach can successfully encode 110 (96%) specifications as compared to 87 (76%) under prior approaches, an improvement of 20 percentage points. We implement the specifications in the form of a runtime monitoring framework to check the compliance of 3 state-of-the-art autonomous vehicles finding that they violated scene flow properties over 40 times in 30 test executions, including 34 violations for failing to yield properly at intersections.
Tue 24 JunDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
10:30 - 12:30 | Verification and ValidationDemonstrations / Ideas, Visions and Reflections / Research Papers / Journal First at Cosmos 3A Chair(s): Alex Orso Georgia Institute of Technology | ||
10:30 10mTalk | TraceMOP: An Explicit-Trace Runtime Verification Tool for Java Demonstrations | ||
10:40 10mTalk | VO-GCSE: Verification Optimization through Global Common Subexpression Elimination Demonstrations Rafael Menezes University of Manchester, Norbert Tihanyi Technology Innovation Institute, Ridhi Jain Technology Innovation Institute (TII), Abu Dhabi, UAE, Alexander Levin Nvidia, Rosiane de Freitas Federal University of Amazonas, Lucas C. Cordeiro University of Manchester, UK and Federal University of Amazonas, Brazil | ||
10:50 10mTalk | GIVUP: Automated Generation and Verification of Textual Process Descriptions Demonstrations Quentin Nivon University Grenoble Alpes, Gwen Salaün University of Grenoble Alpes, Frederic Lang Univ. Grenoble Alpes, Inria, CNRS, Grenoble INP, LIG, Grenoble, France | ||
11:00 10mTalk | NeuroStrata: Harnessing Neuro-Symbolic Paradigms for Improved Testability and Verifiability of Autonomous CPS Ideas, Visions and Reflections Xi Zheng Macquarie University, Ziyang Li University of Pennsylvania, Ivan Ruchkin University of Florida, Ruzica Piskac Yale University, Miroslav Pajic Duke University | ||
11:10 20mTalk | Scene Flow Specifications: Encoding and Monitoring Rich Temporal Safety Properties of Autonomous Systems Research Papers Trey Woodlief University of Virginia, United States, Felipe Toledo , Matthew B Dwyer University of Virginia, Sebastian Elbaum University of Virginia DOI | ||
11:30 20mTalk | QSF: Multi-Objective Optimization based Efficient Solving for Floating-Point Constraints Research Papers Xu Yang College of Computer Science and Technology, National University of Defense Technology, Zhenbang Chen College of Computer, National University of Defense Technology, Wei Dong National University of Defense Technology, Ji Wang National University of Defense Technology DOI | ||
11:50 20mTalk | Consistent Local-First Software: Enforcing Safety and Invariants for Local-First Applications Journal First Mirko Köhler TU Darmstadt, George Zakhour University of St. Gallen, Pascal Weisenburger University of St. Gallen, Guido Salvaneschi University of St. Gallen | ||
12:10 20mTalk | ChangeGuard: Validating Code Changes via Pairwise Learning-Guided Execution Research Papers Lars Gröninger University of Stuttgart, Beatriz Souza Universität Stuttgart, Michael Pradel University of Stuttgart DOI |
Cosmos 3A is the first room in the Cosmos 3 wing.
When facing the main Cosmos Hall, access to the Cosmos 3 wing is on the left, close to the stairs. The area is accessed through a large door with the number “3”, which will stay open during the event.