Transcription
A Tutorial on Runtime Verification andAssuranceAnkush DesaiEECS 219C(
Outline1. Background on Runtime Verification2. Challenges in Programming Robotics System(Drona).3. Solution 1: Combining Model Checking and RuntimeVerification.4. Solution 2: Programming Language with RuntimeAssurance.(PROGRAMMING SAFE ROBOTICS SYSTEMS2
BackgroundFormal Verification (e.g., Model checking): Formal, sound, provides guarantees.Doesn’t scale well - state explosion problem.Checks a model, not an implementation.Most people avoid it – too much effort.Testing (ad-hoc checking): (Most widely used technique in the industry.Scales well, usually inexpensive.Test an implementation directly.Informal, doesn’t provide guarantees.PROGRAMMING SAFE ROBOTICS SYSTEMS3
Runtime VerificationAttempt to bridge the gap between formal methodsand ad-hoc testing. A program is monitored while it is running and checkedagainst properties of interest. Properties are specified in a formal notation (LTL, RegEx,etc.). Dealing only with finite traces.Considered as a light-weight formal methodtechnique. Testing with formal “flavour”. Still doesn’t provide full guarantees.(PROGRAMMING SAFE ROBOTICS SYSTEMS4
Runtime Verification, cont’dHow to monitor a program? Need to extract events from the program while it is running. code instrumentation.ProgramStatic phaseCodeInstrumentationSpecificationsDynamic phaseRuntimeChecker(Stream of eventsInstrumentedProgram5
Still, What is Runtime Verification?There are three interpretations of what runtime verification is, incontrast with formal verification discussed in this course.1. RV as lightweight verification, non-exhaustive simulation (testing) plusformal specifications2. RV as getting closer to implementation, away from abstract models.3. RV as checking systems after deployment while they are up and running.(PROGRAMMING SAFE ROBOTICS SYSTEMS6
RV as Lightweight Formal Methods Verification is glorious and romantic but practically hardbeyond certain complexity. Simulation/testing is here to stay with or withoutattempts to guarantee some coverage. So let us add to this practice some formal properties andproperty monitors that check the simulation traces. Instead of language inclusion Ls Lϕ as in verification,we check membership w Lϕ, one trace at a time. Monitoring is less sensitive to system complexity. It doesnot require a mathematical model of the system, aprogram or a black box is sufficient. In fact, it does not care who generates the simulationtraces, it could be measurements of a real physicalprocess.(PROGRAMMING SAFE ROBOTICS SYSTEMS7
Main Challenge: Efficient monitoring1. Low instrumentation communication overhead.2. An efficient monitor should have the followingproperties: No backtracking. Memory-less: doesn’t store the trace. Space efficiency. Runtime efficiency. (A monitor that runs in time exponential in the size of the trace isunacceptable.A monitor that runs in time exponential in the size of the formula isusable, but should be avoided.8
PROGRAMMING SAFE ROBOTICS SYSTEMS(PROGRAMMING SAFE ROBOTICS SYSTEMS9
Autonomous Mobile RoboticsA major challenge in autonomous mobile roboticsWarehouseis programmingrobotsSurveillancewith formal guarantees and high assurance of correctoperation.Delivery Systems(AgricultureDRONA10
“If you are able to verify a robotics systemthen most likely something is wrong”-Russ Tedrake, MIT(DRONA11
Surveillance ApplicationWorkspace in Gazebo Simulator(Obstacle Map and Drone TrajectoryDRONA12
Robotics Software Stack(CAV’15DRONA13
Robotics SoftwareRobotics Software for such an autonomous drone is highly complex, reactiveand concurrent.armDisarmed(on issionPlanExecutorcriticalBatteryMonitorsModes of Operation of the Surveillance Drone(DRONASurveillance Mode14
Our Approach1. Programming Frameworkfor Reactive Systems: P Programming Language.Surveillance ProtocolApplication2. Scalable Analysis ofRobotics Software usingModel Checking. Using discreteabstractions of the robotbehavior.OnlineMonitorsRV ModulePlan ExecutorTrusted Software Stack3. Use Runtime Monitoring toensure that the assumptionhold.(MachineLearningModulesMotion PlannerControllersStateEstimatorsRobot SDKDRONA15
Motion Planner Motion Primitive: goto(location)q2q0(qgq1DRONA16
Motion Planner Verify that the plans generated by the motionplanner are always distance away from allobstacles. We used constraint solver (and RRTStar) toimplement the motion planner.(DRONA17
Signal Temporal Logic (STL)Syntax Real‐time and real‐valued temporal logic formulasSemantic Qualitative (Boolean): Is the formula True or False? Quantitative (Real): How robustly is the formula True or False?(DRONA18
Quantitative SemanticsExample STL requirement: Avoid anobstacle f : G[0,5]( x 10 ) Both the paths satisfy therequirement But p1 more robustly than p2(x10p295p1Bool:B(f,p1) TB(f,p2) TReal:R(f,p1) 5R(f,p2) 1DRONA19
Assumptions as STL Formulasqg(DRONA20
Assumptions as STL Formulasq2qgq1(DRONA21
Parameter LearningQuestion: What value of ,to use ?Learn functions: ft, f : R x R - Rduration(,and overshootDRONA,22
Validating Low-Level Controllers(DRONA23
Online STL MonitoringFor each of the assumption about the low-levelcomponents:1. An STL formula is generated corresponding.2. An online monitor is created dynamically tomonitor the STL specification and take preemptiveaction based on the robustness value.(DRONA24
Drona Tool(DRONA25
Results: Reference Trajectory(DRONA26
Results: Obstacle Avoidance(DRONA27
Demo Video(DRONA28
RUNTIME ASSURANCE FOR SAFE ROBOTICS(PROGRAMMING SAFE ROBOTICS SYSTEMS29
Robotics Software Stack(1) Obstacle Avoidance ():The drone must nevercollide with any obstacle.): The(2) Battery Safety (drone must never crashbecause of low battery,instead, when the battery islow it must land safely.(CAV’15DRONA30
Simplex Architecture(PROGRAMMING SAFE ROBOTICS SYSTEMS31
A RTA ModuleA RTA Module is a tuple,, is the Advanced controller. is the Safe controller. ,,Δis a set of states. Δ is the sampling rate of the DM.(PROGRAMMING SAFE ROBOTICS SYSTEMS32
A RTA machine is well-formedA RTA Machineformed:, Outputs ofandand ,,, Δ is well-are the same.have same period ( Δ). Thesatisfies the following properties:1.,, 2. , , . . ,,,,Δ 1., , 2Δ . Note that thiscondition is stronger.(PROGRAMMING SAFE ROBOTICS SYSTEMS33
(PROGRAMMING SAFE ROBOTICS SYSTEMS34
(PROGRAMMING SAFE ROBOTICS SYSTEMS35
Compositional Runtime Assurance(PROGRAMMING SAFE ROBOTICS SYSTEMS36
Untrusted Motion Primitive(PROGRAMMING SAFE ROBOTICS SYSTEMS37
RTA Protected Motion PrimitiveOnly AC 10 secsRTA (AC SC) 14 secsOnly SC 23 secs(PROGRAMMING SAFE ROBOTICS SYSTEMS38
Demo(PROGRAMMING SAFE ROBOTICS SYSTEMS39
A Tutorial on Runtime Verification and Assurance Ankush Desai EECS 219C (Outline 1. Background on Runtime Verification 2. Challenges in Programming Robotics System . Online STL Monitoring For each of the assumption about the low-level components: 1. An STL formula is generated corresponding. 2. An online monitor is created dynamically to
