Tutorial 7: Requirement-driven Testing and Verification for Autonomous Cyber-Physical Systems
Jyotirmoy V. Deshmukh - Univ. of Southern California, Los Angles, CA Souradeep Dutta - Univ. of Colorado, Boulder, CO
Jyotirmoy V. Deshmukh - Univ. of Southern California, Los Angles, CA
This tutorial will introduce the attendees to a range of formal approaches available to engineers designing autonomous cyber-physical systems. Cyber-physical systems are those that use embedded software to control the behavior of physical components. CPS applications include self-driving cars, unmanned aerial vehicles, ground robots, medical devices, internet-of-things devices, transportation and energy distribution infrastructures, among others. As many of these systems are safety-critical, it is urgent to develop design flows that enable developers to use formal requirements to describe the expected high-level behavior of such systems. Over the past few years, there has been a growing ecosystem of tools and We will discuss 5 main topics in this tutorial: (1) choosing the appropriate formalism to express correctness requirements for CPS applications, (2) requirements-driven automatic test generation approaches for logical formalisms such as Signal Temporal Logic, (3) approaches to ease the burden of writing formal requirements and tools to automatically infer requirements from models or data, (4) approaches for efficiently monitoring requirements, and integrating requirements into existing design flows, and finally, (5) techniques to reason about autonomous systems that use AI-based algorithms such as neural networks. We will primarily draw upon the experiences of engineers in the automotive domain in using tools in each of the aspects mentioned above. Wherever appropriate, we will also include examples from other domains such as robotics and medical devices.