Mining Requirements from Closed Loop Control Models Jyotirmoy V. Deshmukh Joint work with: Xiaoqing Jin Alexander Donz Sanjit A. Seshia But, you are doing it all wrong! Arent you supposed to check if design satisfies requirements/specifications/properties? Design Requiremen ts Mining Temporal Requirements from Control Models 2/30 Challenges Closed-loop models very complex:

nonlinear dynamics look-up tables large amounts of switching components with no models unclear semantics Requirements too vague, high-level: intake manifold pressure should settle increase fuel efficiency improve ride quality Mining Temporal Requirements from Control Models 3/30 What this work is all about How we could use formal reasoning when all

Requirem ent Ability to simulate and test system Mining! we have is: Vague idea of what system should satisfy (Possibly limited) ability to check if system Mining Temporal Requirements from Control Models 4/30 Mining in Action As-is properties of closed-loop design Ask designer if mined requirements are OK Settling time is 6.25 ms

Overshoot is 100 units 100 6.25ms Mining Temporal Requirements from Control Models 5/30 Mine for one version, get many free Version 0 Mine Requirements Requirement 1 Requirement 2 Requirement 3 Use for V&V Version 1 Use for V&V Version 2 Mining Temporal Requirements from Control Models

6/30 Use for V&V Legacy code Value added by mining: Mined Requirements become useful documentation Useful for code maintenance and revision Use requirements during tuning and testing Mining Temporal Requirements from Control Models 7/30 Its working, but I dont understand why! Outline

Expressing Requirements in Signal Temporal Logic Mining Algorithm Experimental Results Mining Temporal Requirements from Control Models 8/30 Expressing Requirements in Signal Temporal Logic Mining Temporal Requirements from Control Models 9/30 Signal Temporal Logic (STL)

Extension of Metric Temporal Logic (MTL) Allows tests over continuous-valued signal variables x 3 Examples: 1 0 50 t 100 x 1 +0.1 -0.1 0 Mining Temporal Requirements from Control Models 60

t 100 10/30 Quantitative Semantics of STL Function that maps STL formula to a numeric value Quantifies how much a trace satisfies a property Large positive value : trace easily satisfies Small positive value: trace close to violating Negative value: trace does not satisfy Mining Temporal Requirements from Control Models 11/30

Mining Algorithm Mining Temporal Requirements from Control Models 12/30 CounterExample Guided Inductive Synthesis S YYEES 1. m. 1. Settling Settling Time Time is is 5 5 ms ms Overshoot is 5 KPa Overshoot is 5 KPa Upper

Upper Bound Bound on on x x is is 3.6 3.6 Find Tightest Answers Settling Settling Time Time is is ?? ?? Overshoot is ?? Overshoot is ?? Upper Upper Bound Bound on on x x is is ?? ?? Mining Temporal Requirements from Control Models Are there behaviors that do NOT satisfy these

requirements? 13/30 CounterExample Guided Inductive Synthesis 1. m. S YYEES 1. Are there behaviors that do NOT satisfy these requirements? n. Counterexamples Settling 5.3 ms Settling Time Time is is 5.3ms

ms ms Overshoot is 5.1 KPa KPa Overshoot is 5.1KPa KPa Upper Bound on x 3.8 Upper Bound on x is is 3.8 Find Tightest Answers Settling Settling Time Time is is ?? ?? Overshoot is ??

Overshoot is ?? Upper Upper Bound Bound on on x x is is ?? ?? Mining Temporal Requirements from Control Models 14/30 CounterExample Guided Inductive Synthesis 1. m. Are there behaviors that do NOT satisfy these requirements? 1. n. Counterexamples Find Tightest Answers

Settling Settling Time Time is is ?? ?? Overshoot is ?? Overshoot is ?? Upper Upper Bound Bound on on x x is is ?? ?? Mining Temporal Requirements from Control Models Settling Settling Time Time is is 6.3 6.3 ms ms Overshoot is 5.6 KPa Overshoot is 5.6 KPa Upper

Upper Bound Bound on on x x is is 4.1 4.1 Mined Requireme nt 15/30 NO NO Settling Settling Time Time is is 6.3 6.3 ms ms Overshoot is 5.6 KPa Overshoot is 5.6 KPa Upper Upper Bound Bound on on x x is is 4.1

4.1 Parametric STL Constants in STL formula replaced with parameters Scale parameters Time parameters Examples: Between some time and 10seconds, x remains greater than some value After transmission shifts to gear 2, it remains in gear 2 for at least secs Mining Temporal Requirements from Control Models 16/30 Semantics of PSTL formula (p)

p=( ) Valuation function v assigns values to parameters in p (v(p)) is an STL formula Validity domain: {v(p) | i: (xi,j=t) (v(p))} {xi} : set of traces Mining Temporal Requirements from Control Models 17/30 (I.e. Find the tightest value) Parameter Synthesis x -satisfies property if for some i: (v(p)) (v(p))

(x,t) (x,t) |vi vi| < v(p) = (v1,vi,) v(p) = (v1,vi,) (v(p)) Find -tight valuation v such that i: (xi,0) Multi-criteria, nonlinear optimization problem Solution not unique, need to find Pareto-optimal solution Mining Temporal Requirements from

Control Models 18/30 Parameter Synthesis Nave approach: grid parameter space evaluate satisfaction value at each point pick valuation with smallest satisfaction value Exponential number of points in parameter space Could miss optimal values Mining Temporal Requirements from Control Models

19/30 Satisfaction Monotonicity Sat. value monotonically increasing in ith parameter: x (v(p)) and v(pi) v(pi) and ji v(pj) =v(pj) x (v(p)) Monotonic if either decreasing or increasing 4 3 If upper bound of all signals is 3, any number > 3 is also an upper bound 0 50 100 Binary-search in monotonic parameter dimensions

Now implemented in tool BREACH Mining Temporal Requirements from Control Models 20/30 Checking Monotonicity Checking monotonicity is undecidable Encode monotonicity check as SMT query F.O. Logic with quantifiers + uninterpreted functions + real arithmetic Return yes/ no / unknown If yes proof of monotonicity If no fall back to nave procedure

Mining Temporal Requirements from Control Models 21/30 Falsification: any violating behaviors? u S(u) \ \ (v(p) ) Falsification Tool Mining Temporal Requirements from Control Models 22/30 Falsification as Optimization Solve = min (' ; S(u); 0)

u2 U Nonlinear Optimization Problem, No exact solution, Limited formal guarantees If < 0, found falsifying trace! Use stochastic optimization such as in STALIRO Need clever parameterization ofamplitude input signal Signal parameters: (A), delay (D) space u Implemented parameterization in Breachbased falsifier Mining Temporal Requirements from 23/30

Control Models Mining in a nutshell 1. m. 1. YES YES S-TALIRO/ BREACH falsified Requirement? n. Counterexamples BREACH Candidate Candidate Requirement Requirement Mined

Mined STL STL Requirement Requirement Template Template PSTL PSTL property property Mining Temporal Requirements from Control Models 24/30 NO NO Experimental Results Mining Temporal Requirements from Control Models 25/30 Experimental Results S-TALIRO for Falsification* Upper bounds on speed & rpm Cannot reach 100mph in seconds with rpm <

BREACH for Falsification Time taken # Simulations Time Taken # Simulation s 55 s 255 197 s 496 6422 s 9519 267 s 709

Cannot reach 100mph in seconds with rpm < 8554 s 18284 147 s 411 We ran S-TALIRO with default options and did not explore signal parameterization Minimum Dwell time in Gear 2 18886 s 130 1015 s 431 Mining Temporal Requirements from Control Models 26/30 Experimental Results Experimental Engine Control Model Found max overshoot with 7000 simulations in 13 hours Attempt to mine max settling time:

Stops after 4 iterations with tsettle = total time for simulation Mining Temporal Requirements from Control Models 27/30 Mining can lead to deep bugs Experimental Engine Control Model Each iteration produced intermediate requirements Forced falsification to explore trajectories more likely to altogether violate requirement Discussion with control designer revealed it to be a real bug Root cause identified as wrong value in a look-up table, bug was fixed Why mining could be useful for bug-finding:

Mining provides better direction information to optimizer Looking for bugs Mine for negation of bug Mining Temporal Requirements from Control Models 28/30 References BREACH & STL: 1. 2. 3. Alexander Donz, Oded Maler. Robust satisfaction of temporal logic over realvalued signals. Formal Modeling and Analysis of Timed Systems, 2010. Alexander Donz. Breach: A Toolbox for Verification and Parameter Synthesis of Hybrid Systems. CAV, 2010. Eugene Asarin, Alexander Donz, Oded Maler and D. Nickovic. Parametric identification of temporal properties. Runtime Verification, 2011. S-TALIRO: 1. 2. http://www.eecs.berkeley.edu/~donze/breach_page.html https://sites.google.com/a/asu.edu/s-taliro/s-taliro

Sriram Sankaranarayanan and Georgios Fainekos. Falsification of temporal properties of hybrid systems using the cross-entropy method. HSCC 2012. Y. Annpureddy. C. Liu, G. E. Fainekos, and S. Sankaranarayanan. STaLiRo: A tool for Temporal Logic Falsification for Hybrid Systems: TACAS 2011. Mining Temporal Requirements from Control Models 29/30 Thank You! Mining Temporal Requirements from Control Models 30/30 Backup Slides Mining Temporal Requirements from Control Models Syntax & Semantics Synta x Semantics Mining Temporal Requirements from Control Models

Quantitative Semantics of STL Following (satisfaction value) does the trick Mining Temporal Requirements from Control Models Quantitative Semantics Demystified x 2 1 = x 1:5 0 0.1 0.2 0.3 0.4 0.5 0.6 0.7 1

0.5 -0.5 0.5 -1 0 0.5 1 t 1 sup over each interval Mining Temporal Requirements from Control Models 0.5 0.5 0.5 0.5 0.5

Quantitative Semantics Demystified = 0.5 x 2 1 = x 1:5 0 0.1 0.2 0.3 0.4 0.5 0.6 0.7 1 0.5 -0.5

0.5 -1 0 0.5 1 1 0.5 0.5 0.5 0.5 0.5 0.5 nf over result from previous step Mining Temporal Requirements from Control Models t