The Use of Formal Methods in Verifying Behavior of Autonomous Vehicles Alyssa Byrnes 1 Motivation Car software systems are very complicated...The GM Volt contains +10M lines of code

How do we verify that it behaves correctly? Formal methods add automation to checking this The correctness of a system = expected behavior of the system. 2 How it works Specification

Take existing system. Create a specification of that system. Prove that the specification accurately represents the system. Prove properties about system by proving properties about the specification. 3 What is a specification?

Specification A specification can be regarded as a description that is intended to be as precise, unambiguous, concise, and complete as possible in the contexts of its specific application . A formal specification is a specification written in a formal language[1]

4 Basic Logic Introduction Atoms: A,B{{True, False} Operations: , ,, 5 Temporal Operators Fp - p holds sometime in the future.

Gp - p holds globally in the future. Xp - p holds next time. pUq - p holds until q holds. 6 Model-based vs. Algebraic Specification Model Based

Explicit specification of abstract machines System is specified using mathematical entities (sets, sequences, etc.) and operations are defined by how they affect those states. Algebraic/Property-Oriented

Abstract data types specified by axioms defining relationships between its operations 7 Main Methods of Formal Verification Model checkers Symbolic Executers Theorem Provers

8 Model Checkers A model checker verifies a system against a set of specified properties. Usually the system is specified as a set of finite state machines, and the properties are expressed using a temporal logic. The model is typically built in one language, and then verified using a separate model checker.

9 Model Checker Example Example property: The oven doesnt heat up until the door is closed. ( heat_up) U door_closed 10

Probabilistic Model Checking[8] Models are represented as Markov Chains. Discrete-time Markov Chains:

discrete set of states representing possible system configurations transitions between states occur in discrete time-steps probability of making transitions between states is given by discrete probability distributions Properties expressed in Probabilistic Computation Tree Logic (PCTL)

Temporal logic for describing properties of DTMCs/MDPs Extension of (non-probabilistic) temporal logic CTL Example send P0.95 [ F10 deliver ] if a message is sent, then the probability of it being delivered within 10 steps is at least 0.95

11 Symbolic Executer Symbolic assignments At branch instructions Explore all satisfiable paths Recorded in path constraint

Tree of execution states is created 12 13 Theorem Provers Find a proof for a given set of

axioms and inference rules. Usually involve a lot of user interaction. Often utilize symbolic execution and model checking. 14 Coq Demonstration Here, I will switch tabs to perform a basic demonstration of the functions of the theorem prover Coq using the Coq

IDE. 15 Verifying Autonomous Systems Most work has implemented model checking. Two methods to verify a complex system: Build an implementable model of the system using formal methods. Develop an accurate model representation of an

existing system using formal methods. 16 Where formal verification is used [4] 17 Rational Agents The autonomous systems are conceptualized as

rational agents, or agents with explicits reasons for making the choices it does, and the ability to explain them. Rational agent architecture is made up of Beliefs, Desires, and Intentions. Beliefs: Agents information about itself, other agents, and its environment. Desires: Long-term goals. Intentions: Goals the agent is actively pursuing.

18 What are we verifying? Since it is hard to predict all possible environmental outcomes of an autonomous vehicle, common

practice is to instead focus on what decisions the vehicle makes verifying properties about those decisions. Want to show: vehicle is making best possible decisions based on an accurate representation of the environment. In other words: [4] 19 Work that has been done:

A lot of work has gone towards verifying Unmanned Aircraft Systems (UAS), or a group of elements necessary to enable the autonomous flight of at least one Unmanned Air Vehicle (UAV)[5]. 20 Verifying UASs, approach:

21 Verifying UASs, architecture: 22 Properties Verified: 23

Applying this to Semiautonomous Cars Driggs-Campbell et al. have done work to create a model of a car that incorporates formal methods to certain aspects of the vehicle. This includes creating a model of a semiautonomous car and a formal model of the driver. [6, 7] 24

Semiautonomous Model: Vehicle Framework 25 Modeling Vehicle Motion Safety Constraints: 26

Probabilistic Modeling and Verification of Human Behavior Model: Convex-Markov Chain; Logic: Probabilistic Computation Tree Logic A linearized vehicle model is used to generate a trajectory set. Probability intervals are generated using a determined confidence level.

27 Model of A Complex Maneuver 28 Showing Effectiveness 29

Thank you for your attention! Sources: 1. 2. 3. 4. 5. 6. 7. 8.

http://www.cs.cmu.edu/~modelcheck/tour.htm http://www.cs.cmu.edu/~emc/15-398/lectures/overview.pdf http://www.cs.ucr.edu/~heng/teaching/cs260-winter2017/symexec.pdf http://cgi.csc.liv.ac.uk/~matt/pubs/cacm2013preprint.pdf https://link.springer.com/chapter/10.1007/978-3-642-24270-0_17 http://www.me.berkeley.edu/~frborrel/pdfpub/victor.pdf http://human-cps.eecs.berkeley.edu/AAAI2014.pdf http://www.prismmodelchecker.org/lectures/pmc/01-intro.pdf

30