Formal Specification and Verification of Autonomous Vehicle Control System

Formal Specification and Verification of an Autonomous Vehicle Control System by the OTS/CafeOBJ method Yifan, Wang (Toyama Prefectural University) Nakamura, Masaki (Toyama Prefectural University) Sakakibara, Kazutoshi (Toyama Prefectural University) 1 SEKE 2023

Background Acceleration of urbanization in various countries Smart cities with only autonomous vehicles are expected Need to establish basic technologies to obtain reliable and efficient autonomous vehicles https://masdar.ae https://www.woven-city.global 2 SEKE 2023

Background A hybrid system is a dynamic system that includes both continuous and discrete dynamic behavior. The autonomous vehicle has both continuous behaviors (velocity and position) and discrete behaviors (pedal actions) To design and verify an autonomous vehicle control system we model it as a hybrid system Control theory Computer science infinite State machines Continuous Dynamical system Hybrid system 3 SEKE 2023

Technologies for analyzing autonomous vehicle behaviors There are many techniques used to test and simulate autonomous vehicles, such as CarMaker, SUMO Only testing and simulation just provide some kinds of limited or predetermined paths, it is far from enough for safety We need formal approaches to make sure safety of autonomous vehicles 4 CarMaker: https://www.fsi-embedded.jp/carmaker/view/ SUMO: https://www.eclipse.org/sumo/ SEKE 2023

Formal method Formal verification is an approach to verify a given specification One approach of formal verification is model checking, it is fully automated but the state space is limited The other approach of formal verification is theorem proving, it is semi-automated but applicable to infinite state space Formal method Formal verification Formal specification Model checking Theorem proving Model checking 5 SEKE 2023

CafeOBJ specification language CafeOBJ supports specification execution based on a rewrite theory for theorem proving The OTS/CafeOBJ method is a formal method in which a system is modeled as an observational transition system (OTS), Its specification is described in CafeOBJ, and properties are verified formally based on the specification execution, called the proof score method https://cafeobj.org 6 SEKE 2023

Our approach In this study, we propose a way to describe a formal specification of an autonomous vehicle control system in CafeOBJ algebraic specification language The control system is a hybrid system with continuous variables of time, velocity, and position controlled by discrete pedal actions including acceleration, braking, and no-operation(nothing) We also verify the safety property of the autonomous vehicle control system by a theorem proving technique called the proof score method Modeling initial VEHICLE Specification Verification open ISTEP . op t1 : -> Rat . eq c-tick(t1,s) = true . eq s' = tick(t1,s) . eq loc1(s) = accel . eq (0 <=(t1 + v1(s))) = true . eq ((t1 + v1(s)) <= 4) = true . eq ((v1(s) * t1 + 1/2 * t1 * t1 + x1(s)) <= 36) = true . red istep1 . close eq (((- t1) + v1(s)) <= 4) = true . red istep1 . close open ISTEP . op t1 : -> Rat . eq c-tick(t1,s) = true . eq s' = tick(t1,s) . eq loc1(s) = nothing . eq v1(s) = 0 . red istep1 . close true . open ISTEP . op t1 : -> Rat . eq c-tick(t1,s) = true . eq s' = tick(t1,s) . eq loc1(s) = brake . eq (0 <= ((- t1) + v1(s))) = A B N RAT LABEL 7 SEKE 2023

Hybrid autonomous vehicles system We consider a hybrid automaton of an autonomous vehicle control system and assume there is an obstacle at position 45 We give the vehicle initial state, and limitation of the velocity and position in three locations Brake, Accelerate and Nothing 8 SEKE 2023

Initial state in CafeOBJ In our OTS model there are four observations and four transitions Observations loc1, x1, v1 and now observe the values of discrete and continuous variables Initial state is defined by loc1, x1, v1 and now eq loc1(init) = accel . eq now(init) = 0 . eq v1(init) = 0 . eq x1(init) = 0 . op init : -> Sys bop loc1 : Sys -> Label bops x1 v1 now : Sys -> Rat 9 SEKE 2023

Discrete Transition in CafeOBJ A transition is also defined through observations Transitions tick, a, b and n change the values of those observations A term b(S) denotes the result state by applying the transition b to the state S eq loc1(b(S)) = brake . eq now(b(S)) = now(S) . eq v1(b(S)) = v1(S) . eq x1(b(S)) = x1(S) . 10 SEKE 2023

Continuous Transition in CafeOBJ We specify the time advancing tick by observations if they satisfy the c-tick The operation nextv(V,A,T) and nextx(X,V,A,T) calculate the value of v1 and x1 after T from the state ceq now(tick(T,S)) = now(S) + T if c-tick(T,S) . ceq v1(tick(T,S)) = nextv(v1(S), a1(loc1(S)), T) if c-tick(T,S) . ceq x1(tick(T,S)) = nextx(x1(S), v1(S), a1(loc1(S)), T) if c-tick(T,S) . eq nextv(V,A,T) = V + A * T . eq nextx(X,V,A,T) = V * T + 1/2 * A * T * T + X . 11 SEKE 2023

Define condition of tick(c-tick) The effective condition c-tick is defined from invariants to keep the velocity could not exceed 4 and the position could not exceed 44 (we assume that there is an obstacle at position 45 and need to reduce the velocity from position 36) eq c-tick(T,S) = (loc1(S) = brake implies (0 <= nextv(v1(S), a1(loc1(S)), T) and nextv(v1(S), a1(loc1(S)), T) <= 4)) and (loc1(S) = accel implies ((0 <= nextv(v1(S), a1(loc1(S)), T) and nextv(v1(S), a1(loc1(S)), T) <= 4) and (nextx(x1(S), v1(S), a1(loc1(S)), T) <= 36))) and (loc1(S) = nothing implies (((0 < nextv(v1(S), a1(loc1(S)), T) and nextv(v1(S), a1(loc1(S)), T) <= 4) and (nextx(x1(S), v1(S), a1(loc1(S)), T) <= 36)) or (nextv(v1(S), a1(loc1(S)), T) = 0))) . 12

Theorem proving for the safety property For verification, we declare a predicate inv1 denotes that position x1 does not exist over 45 when the vehicle at S By the proof score method, we prove the property by the induction on the structure of reachable states mod INV{ pr(VEHICLE) op inv1 : Sys -> Bool var S : Sys vars V A X T : Rat eq inv1(S) = (x1(S) < 45) . } 13 SEKE 2023

Theorem proving for the safety property Base case: Prove inv1 for the initial state and the proof script returns true open INV . red inv1(init) . close -- opening module INV done. -- reduce in %INV : (inv1(init)):Bool (true):Bool 14 SEKE 2023

Induction step We prove inv1 for the state ?(s) for all transition ? under the induction hypothesis inv1(s) Unfortunately, it does not return true We introduce case splitting and introducing lemma to obtain a complete proof mod ISTEP{ pr(INV) . op istep1 : -> Bool ops s s' : -> Sys eq istep1 = inv1(s) implies inv1(s ) . } open ISTEP . op t1 : -> Rat . eq s' = tick(t1,s) . red istep1(p) . Close 15 SEKE 2023

Complete proof We proved inv by introducing 2 lemmas eq inv1(S) = (x1(S) < 45) . eq inv2(S) = (x1(S) <= -1/2 * v1(S) * v1(S) + 44) . We proved inv by introducing 10 cases(reachable states) open ISTEP . op t1 : -> Rat . eq c-tick(t1,s) = true . eq s' = tick(t1,s) . eq loc1(s) = accel . eq (0 <=(t1 + v1(s))) = true . eq ((t1 + v1(s)) <= 4) = true . eq ((v1(s) * t1 + 1/2 * t1 * t1 + x1(s)) <= 36) = true . red istep1 . close open ISTEP . . . . . . . red istep2 . close 16 SEKE 2023

Conclusion We described an observational transition system of an autonomous vehicle control system as an example of a hybrid system, and verified the safety property by the proof score method One of our future works is to apply the proposed method to practical applications of multitask hybrid systems with multiple autonomous vehicles 17 SEKE 2023