Combining CEGAR and Lazy Abstraction for Verifying Timed Systems

Timed automata with clocks and data variables are a widely used formalism for modeling timed systems with complex behaviors. Counterexample-guided abstraction refinement (CEGAR) and lazy abstraction can both construct an abstract state space representation: CEGAR supports a wide set of expressive data abstractions, but only few refinement techniques for clocks, in contrast, lazy abstraction is more efficient for time abstraction. We present a combined abstraction refinement technique to take advantage of the benefits of CEGAR for data variables and lazy abstraction for clocks.

Transcript

1. Combining CEGAR and Lazy Abstraction for Verifying Timed Systems Dóra Cziborová Alpine Verification Meeting 2023
2. Combining CEGAR and Lazy Abstraction for Verifying Timed Systems 2 • Complex timed behaviors and computations with external data (sensor inputs) • System models specified by higher-level formalisms, e.g., – XTA composite models – Block diagrams and timed statecharts from systems engineering tools • Examples: railway communication protocols, safety-critical automotive subsystems Verification of Timed Systems by Model Checking System Requirement Formalized requirement Formal model Model checker 🗸 ✗ Real-time software-intensive systems
3. Combining CEGAR and Lazy Abstraction for Verifying Timed Systems 3 Verification of Timed Systems by Model Checking System Requirement Formalized requirement Formal model Model checker 🗸 ✗ measure error check timeout 𝑐 ≤ 0.15 c > 0.05 ℎ𝑎𝑣𝑜𝑐 𝑎𝑛𝑔𝑙𝑒 −360 ≤ 𝑎𝑛𝑔𝑙𝑒 𝑎𝑛𝑔𝑙𝑒 ≤ 360 𝑐 ≤ 0.5 𝑐 ≥ 0.5 ℎ𝑎𝑣𝑜𝑐 𝑐𝑟𝑜𝑠𝑠𝐶ℎ𝑒𝑐𝑘 −360 ≤ 𝑐𝑟𝑜𝑠𝑠𝐶ℎ𝑒𝑐𝑘 𝑐𝑟𝑜𝑠𝑠𝐶ℎ𝑒𝑐𝑘 ≤ 360 𝑐𝑟𝑜𝑠𝑠𝐶ℎ𝑒𝑐𝑘 == 𝑎𝑛𝑔𝑙𝑒 𝑟𝑒𝑠𝑒𝑡(𝑐) ℎ𝑎𝑣𝑜𝑐 𝑐𝑟𝑜𝑠𝑠𝐶ℎ𝑒𝑐𝑘 −360 ≤ 𝑐𝑟𝑜𝑠𝑠𝐶ℎ𝑒𝑐𝑘 𝑐𝑟𝑜𝑠𝑠𝐶ℎ𝑒𝑐𝑘 ≤ 360 𝑐𝑟𝑜𝑠𝑠𝐶ℎ𝑒𝑐𝑘 ! = 𝑎𝑛𝑔𝑙𝑒 Transition system with data and clock variables Running example: simplified model of redundant automotive sensor 𝑎𝑛𝑔𝑙𝑒 ≔ 0 𝑐𝑟𝑜𝑠𝑠𝐶ℎ𝑒𝑐𝑘 ≔ 0
4. Combining CEGAR and Lazy Abstraction for Verifying Timed Systems 4 Verification of Timed Systems by Model Checking System Requirement Formalized requirement Formal model Model checker 🗸 ✗ measure error check timeout 𝑐 ≤ 0.15 c > 0.05 ℎ𝑎𝑣𝑜𝑐 𝑎𝑛𝑔𝑙𝑒 −360 ≤ 𝑎𝑛𝑔𝑙𝑒 𝑎𝑛𝑔𝑙𝑒 ≤ 360 𝑐 ≤ 0.5 𝑐 ≥ 0.5 ℎ𝑎𝑣𝑜𝑐 𝑐𝑟𝑜𝑠𝑠𝐶ℎ𝑒𝑐𝑘 −360 ≤ 𝑐𝑟𝑜𝑠𝑠𝐶ℎ𝑒𝑐𝑘 𝑐𝑟𝑜𝑠𝑠𝐶ℎ𝑒𝑐𝑘 ≤ 360 𝑐𝑟𝑜𝑠𝑠𝐶ℎ𝑒𝑐𝑘 == 𝑎𝑛𝑔𝑙𝑒 𝑟𝑒𝑠𝑒𝑡(𝑐) ℎ𝑎𝑣𝑜𝑐 𝑐𝑟𝑜𝑠𝑠𝐶ℎ𝑒𝑐𝑘 −360 ≤ 𝑐𝑟𝑜𝑠𝑠𝐶ℎ𝑒𝑐𝑘 𝑐𝑟𝑜𝑠𝑠𝐶ℎ𝑒𝑐𝑘 ≤ 360 𝑐𝑟𝑜𝑠𝑠𝐶ℎ𝑒𝑐𝑘 ! = 𝑎𝑛𝑔𝑙𝑒 Transition system with data and clock variables Running example: simplified model of redundant automotive sensor Sensor input replaced by nondeterminism Communication replaced by nondeterminism 𝑎𝑛𝑔𝑙𝑒 ≔ 0 𝑐𝑟𝑜𝑠𝑠𝐶ℎ𝑒𝑐𝑘 ≔ 0
5. Combining CEGAR and Lazy Abstraction for Verifying Timed Systems 5 1) Data variables: • State space explosion 2) Clock variables: • Continuous variables • Reasoning with an uncountably infinite set of states Challenges of Verifying Timed Systems Running example: simplified model of redundant automotive sensor measure error check timeout 𝑐 ≤ 0.15 c > 0.05 ℎ𝑎𝑣𝑜𝑐 𝑎𝑛𝑔𝑙𝑒 −360 ≤ 𝑎𝑛𝑔𝑙𝑒 𝑎𝑛𝑔𝑙𝑒 ≤ 360 𝑐 ≤ 0.5 𝑐 ≥ 0.5 ℎ𝑎𝑣𝑜𝑐 𝑐𝑟𝑜𝑠𝑠𝐶ℎ𝑒𝑐𝑘 −360 ≤ 𝑐𝑟𝑜𝑠𝑠𝐶ℎ𝑒𝑐𝑘 𝑐𝑟𝑜𝑠𝑠𝐶ℎ𝑒𝑐𝑘 ≤ 360 𝑐𝑟𝑜𝑠𝑠𝐶ℎ𝑒𝑐𝑘 == 𝑎𝑛𝑔𝑙𝑒 𝑟𝑒𝑠𝑒𝑡(𝑐) ℎ𝑎𝑣𝑜𝑐 𝑐𝑟𝑜𝑠𝑠𝐶ℎ𝑒𝑐𝑘 −360 ≤ 𝑐𝑟𝑜𝑠𝑠𝐶ℎ𝑒𝑐𝑘 𝑐𝑟𝑜𝑠𝑠𝐶ℎ𝑒𝑐𝑘 ≤ 360 𝑐𝑟𝑜𝑠𝑠𝐶ℎ𝑒𝑐𝑘 ! = 𝑎𝑛𝑔𝑙𝑒 𝑎𝑛𝑔𝑙𝑒 ≔ 0 𝑐𝑟𝑜𝑠𝑠𝐶ℎ𝑒𝑐𝑘 ≔ 0
6. Combining CEGAR and Lazy Abstraction for Verifying Timed Systems 6 Abstraction-based methods: • An abstract state may represent multiple concrete states • State space exploration: abstract reachability graph (ARG) of abstract states and transitions Abstraction, Abstract Reachability Graph
7. Combining CEGAR and Lazy Abstraction for Verifying Timed Systems 7 Abstract Domains Zone abstraction Explicit value abstraction Predicate abstraction
8. Combining CEGAR and Lazy Abstraction for Verifying Timed Systems 8 Abstract Domain for Time Abstraction Zone abstraction 𝑐2 𝑐1 𝑐1 ≤ 7 𝑐1 ≥ 1 𝑐2 < 4 𝑐2 ≥ 0 𝑐2 − 𝑐1 < 1 𝑐1 − 𝑐2 < 5 𝑍 𝑍 A set of clock valuations The same set of clock valuations as a set of clock constraints
9. Combining CEGAR and Lazy Abstraction for Verifying Timed Systems 9 CEGAR (CounterExample-Guided Abstraction Refinement) Refiner 🗸 ✗ Abstract counterexample Refined precision Initial precision Abstractor ARG build prune
10. Combining CEGAR and Lazy Abstraction for Verifying Timed Systems 10 CEGAR (CounterExample-Guided Abstraction Refinement) Refiner 🗸 ✗ Abstract counterexample Refined precision Initial precision Abstractor ARG build prune Builds the ARG with given precision
11. Combining CEGAR and Lazy Abstraction for Verifying Timed Systems 11 CEGAR (CounterExample-Guided Abstraction Refinement) Refiner 🗸 ✗ Abstract counterexample Refined precision Initial precision Abstractor ARG build prune Builds the ARG with given precision Precision e.g. a set of predicates 𝜋 = 𝑝, 𝑞
12. Combining CEGAR and Lazy Abstraction for Verifying Timed Systems 12 CEGAR (CounterExample-Guided Abstraction Refinement) Refiner 🗸 ✗ Abstract counterexample Refined precision Initial precision Abstractor ARG build prune Builds the ARG with given precision Checks feasibility of counterexample Precision e.g. a set of predicates 𝜋 = 𝑝, 𝑞
13. Combining CEGAR and Lazy Abstraction for Verifying Timed Systems 13 CEGAR (CounterExample-Guided Abstraction Refinement) Refiner 🗸 ✗ Abstract counterexample Refined precision Initial precision Abstractor ARG build prune Builds the ARG with given precision Checks feasibility of counterexample Precision e.g. a set of predicates 𝜋′ = 𝑝, 𝑞, 𝑟 𝜋 = 𝑝, 𝑞
14. 14 Lazy Abstraction 🗸 ✗ Lazy Abstractor ARG build Refinement Abstraction Combining CEGAR and Lazy Abstraction for Verifying Timed Systems
15. 15 Lazy Abstraction Nodes with concrete and abstract labels 🗸 ✗ Lazy Abstractor ARG build Refinement Abstraction Combining CEGAR and Lazy Abstraction for Verifying Timed Systems
16. 16 Lazy Abstraction Nodes with concrete and abstract labels 🗸 ✗ Lazy Abstractor ARG build Refinement Abstraction measure check 𝑐 ≤ 0.15 c > 0.05 𝑐 ≤ 0.5 Loc. measure C. 𝑐 ≥ 0 ∧ 𝑐 ≤ 0.15 A. 𝑐 ≥ 0   Combining CEGAR and Lazy Abstraction for Verifying Timed Systems
17. 17 Lazy Abstraction Nodes with concrete and abstract labels 🗸 ✗ Lazy Abstractor ARG build Refinement Abstraction measure check 𝑐 ≤ 0.15 c > 0.05 𝑐 ≤ 0.5 Loc. measure C. 𝑐 ≥ 0 ∧ 𝑐 ≤ 0.15 A. 𝑐 ≥ 0   Without over- approximation Combining CEGAR and Lazy Abstraction for Verifying Timed Systems
18. 18 Lazy Abstraction Nodes with concrete and abstract labels 🗸 ✗ Lazy Abstractor ARG build Refinement Abstraction measure check 𝑐 ≤ 0.15 c > 0.05 𝑐 ≤ 0.5 Loc. measure C. 𝑐 ≥ 0 ∧ 𝑐 ≤ 0.15 A. 𝑐 ≥ 0   Without over- approximation Initialized as abstract as possible Combining CEGAR and Lazy Abstraction for Verifying Timed Systems
19. 19 Lazy Abstraction Nodes with concrete and abstract labels 🗸 ✗ Lazy Abstractor ARG build Refinement Abstraction measure check 𝑐 ≤ 0.15 c > 0.05 𝑐 ≤ 0.5 Loc. measure C. 𝑐 ≥ 0 ∧ 𝑐 ≤ 0.15 A. 𝑐 ≥ 0   Loc. check C. 𝑐 > 0.05 ∧ 𝑐 ≤ 0.5 A. 𝑐 ≥ 0   Without over- approximation Initialized as abstract as possible Combining CEGAR and Lazy Abstraction for Verifying Timed Systems
20. 20 Lazy Abstraction Nodes with concrete and abstract labels 🗸 ✗ Lazy Abstractor ARG build Refinement Abstraction Not parameterized by precision measure check 𝑐 ≤ 0.15 c > 0.05 𝑐 ≤ 0.5 Loc. measure C. 𝑐 ≥ 0 ∧ 𝑐 ≤ 0.15 A. 𝑐 ≥ 0   Loc. check C. 𝑐 > 0.05 ∧ 𝑐 ≤ 0.5 A. 𝑐 ≥ 0   Without over- approximation Initialized as abstract as possible Combining CEGAR and Lazy Abstraction for Verifying Timed Systems
21. 21 Lazy Abstraction Nodes with concrete and abstract labels 🗸 ✗ Lazy Abstractor ARG build Refinement Abstraction Maintains the ARG properties - correctness Not parameterized by precision measure check 𝑐 ≤ 0.15 c > 0.05 𝑐 ≤ 0.5 Loc. measure C. 𝑐 ≥ 0 ∧ 𝑐 ≤ 0.15 A. 𝑐 ≥ 0   Loc. check C. 𝑐 > 0.05 ∧ 𝑐 ≤ 0.5 A. 𝑐 ≥ 0   Without over- approximation Initialized as abstract as possible Combining CEGAR and Lazy Abstraction for Verifying Timed Systems
22. 22 Lazy Abstraction Nodes with concrete and abstract labels 🗸 ✗ Lazy Abstractor ARG build Refinement Abstraction The ARG is complete A counterexample is found Maintains the ARG properties - correctness Not parameterized by precision measure check 𝑐 ≤ 0.15 c > 0.05 𝑐 ≤ 0.5 Loc. measure C. 𝑐 ≥ 0 ∧ 𝑐 ≤ 0.15 A. 𝑐 ≥ 0   Loc. check C. 𝑐 > 0.05 ∧ 𝑐 ≤ 0.5 A. 𝑐 ≥ 0   Without over- approximation Initialized as abstract as possible Combining CEGAR and Lazy Abstraction for Verifying Timed Systems
23. 23 Combining CEGAR and Lazy Abstraction for Verifying Timed Systems CEGAR Lazy abstraction Efficient, supports a wide set of expressive abstractions Either inefficient refinement techniques, or has limited expressiveness Time abstraction Data abstraction Efficient abstraction and refinement techniques Requires defining precision → inefficient refinement techniques
24. 24 Combining CEGAR and Lazy Abstraction for Verifying Timed Systems CEGAR Lazy abstraction Efficient, supports a wide set of expressive abstractions Either inefficient refinement techniques, or has limited expressiveness Time abstraction Data abstraction Efficient abstraction and refinement techniques Requires defining precision → inefficient refinement techniques
25. Combining CEGAR and Lazy Abstraction for Verifying Timed Systems 25 CEGAR on data projection, lazy abstraction on time projection Combining CEGAR and Lazy Abstraction 🗸 ✗ Abstract counterexample Refiner Refined data precision Initial data precision Abstractor Lazy Time Abstractor Lazy Time Refiner Eager Data Abstractor Eager Data Refiner ARG   build prune 
26. Combining CEGAR and Lazy Abstraction for Verifying Timed Systems 26 CEGAR on data projection, lazy abstraction on time projection Combining CEGAR and Lazy Abstraction 🗸 ✗ Abstract counterexample Refiner Refined data precision Initial data precision Abstractor Lazy Time Abstractor Lazy Time Refiner Eager Data Abstractor Eager Data Refiner ARG   build prune  Concrete and abstract time labels Abstract data labels
27. Combining CEGAR and Lazy Abstraction for Verifying Timed Systems 27 CEGAR on data projection, lazy abstraction on time projection Combining CEGAR and Lazy Abstraction 🗸 ✗ Abstract counterexample Refiner Refined data precision Initial data precision Abstractor Lazy Time Abstractor Lazy Time Refiner Eager Data Abstractor Eager Data Refiner ARG   build prune  With given precision Not parameterized by precision Concrete and abstract time labels Abstract data labels
28. Combining CEGAR and Lazy Abstraction for Verifying Timed Systems 28 CEGAR on data projection, lazy abstraction on time projection Combining CEGAR and Lazy Abstraction 🗸 ✗ Abstract counterexample Refiner Refined data precision Initial data precision Abstractor Lazy Time Abstractor Lazy Time Refiner Eager Data Abstractor Eager Data Refiner ARG   build prune  Strengthens the abstract time labels With given precision Not parameterized by precision Concrete and abstract time labels Abstract data labels
29. Combining CEGAR and Lazy Abstraction for Verifying Timed Systems 29 CEGAR on data projection, lazy abstraction on time projection Combining CEGAR and Lazy Abstraction 🗸 ✗ Abstract counterexample Refiner Refined data precision Initial data precision Abstractor Lazy Time Abstractor Lazy Time Refiner Eager Data Abstractor Eager Data Refiner ARG   build prune  Strengthens the abstract time labels Checks feasibility of CEX on the data abstraction With given precision Not parameterized by precision Concrete and abstract time labels Abstract data labels
30. Combining CEGAR and Lazy Abstraction for Verifying Timed Systems Combining CEGAR and Lazy Abstraction   Running example: simplified model of redundant automotive sensor measure error check timeout 𝑐 ≤ 0.15 c > 0.05 ℎ𝑎𝑣𝑜𝑐 𝑎𝑛𝑔𝑙𝑒 −360 ≤ 𝑎𝑛𝑔𝑙𝑒 𝑎𝑛𝑔𝑙𝑒 ≤ 360 𝑐 ≤ 0.5 𝑐 ≥ 0.5 ℎ𝑎𝑣𝑜𝑐 𝑐𝑟𝑜𝑠𝑠𝐶ℎ𝑒𝑐𝑘 −360 ≤ 𝑐𝑟𝑜𝑠𝑠𝐶ℎ𝑒𝑐𝑘 𝑐𝑟𝑜𝑠𝑠𝐶ℎ𝑒𝑐𝑘 ≤ 360 𝑐𝑟𝑜𝑠𝑠𝐶ℎ𝑒𝑐𝑘 == 𝑎𝑛𝑔𝑙𝑒 𝑟𝑒𝑠𝑒𝑡(𝑐) ℎ𝑎𝑣𝑜𝑐 𝑐𝑟𝑜𝑠𝑠𝐶ℎ𝑒𝑐𝑘 −360 ≤ 𝑐𝑟𝑜𝑠𝑠𝐶ℎ𝑒𝑐𝑘 𝑐𝑟𝑜𝑠𝑠𝐶ℎ𝑒𝑐𝑘 ≤ 360 𝑐𝑟𝑜𝑠𝑠𝐶ℎ𝑒𝑐𝑘 ! = 𝑎𝑛𝑔𝑙𝑒 𝑎𝑛𝑔𝑙𝑒 ≔ 0 𝑐𝑟𝑜𝑠𝑠𝐶ℎ𝑒𝑐𝑘 ≔ 0 30
31. Combining CEGAR and Lazy Abstraction for Verifying Timed Systems Combining CEGAR and Lazy Abstraction Loc. measure 𝑝 C. 𝑐 ≥ 0 ∧ 𝑐 ≤ 0.15 A. 𝑐 ≥ 0      Running example: simplified model of redundant automotive sensor measure error check timeout 𝑐 ≤ 0.15 c > 0.05 ℎ𝑎𝑣𝑜𝑐 𝑎𝑛𝑔𝑙𝑒 −360 ≤ 𝑎𝑛𝑔𝑙𝑒 𝑎𝑛𝑔𝑙𝑒 ≤ 360 𝑐 ≤ 0.5 𝑐 ≥ 0.5 ℎ𝑎𝑣𝑜𝑐 𝑐𝑟𝑜𝑠𝑠𝐶ℎ𝑒𝑐𝑘 −360 ≤ 𝑐𝑟𝑜𝑠𝑠𝐶ℎ𝑒𝑐𝑘 𝑐𝑟𝑜𝑠𝑠𝐶ℎ𝑒𝑐𝑘 ≤ 360 𝑐𝑟𝑜𝑠𝑠𝐶ℎ𝑒𝑐𝑘 == 𝑎𝑛𝑔𝑙𝑒 𝑟𝑒𝑠𝑒𝑡(𝑐) ℎ𝑎𝑣𝑜𝑐 𝑐𝑟𝑜𝑠𝑠𝐶ℎ𝑒𝑐𝑘 −360 ≤ 𝑐𝑟𝑜𝑠𝑠𝐶ℎ𝑒𝑐𝑘 𝑐𝑟𝑜𝑠𝑠𝐶ℎ𝑒𝑐𝑘 ≤ 360 𝑐𝑟𝑜𝑠𝑠𝐶ℎ𝑒𝑐𝑘 ! = 𝑎𝑛𝑔𝑙𝑒 𝑎𝑛𝑔𝑙𝑒 ≔ 0 𝑐𝑟𝑜𝑠𝑠𝐶ℎ𝑒𝑐𝑘 ≔ 0 Precision: 𝜋 = 𝑝 𝑝 = 𝑐𝑟𝑜𝑠𝑠𝐶ℎ𝑒𝑐𝑘 == 𝑎𝑛𝑔𝑙𝑒 31
32. Combining CEGAR and Lazy Abstraction for Verifying Timed Systems Combining CEGAR and Lazy Abstraction Precision: 𝜋 = 𝑝 𝑝 = 𝑐𝑟𝑜𝑠𝑠𝐶ℎ𝑒𝑐𝑘 == 𝑎𝑛𝑔𝑙𝑒 Loc. measure 𝑝 C. 𝑐 ≥ 0 ∧ 𝑐 ≤ 0.15 A. 𝑐 ≥ 0    Loc. check 𝑝 C. 𝑐 > 0.05 ∧ 𝑐 ≤ 0.5 A. 𝑐 ≥ 0    Loc. check ¬𝑝 C. 𝑐 > 0.05 ∧ 𝑐 ≤ 0.5 A. 𝑐 ≥ 0    Running example: simplified model of redundant automotive sensor measure error check timeout 𝑐 ≤ 0.15 c > 0.05 ℎ𝑎𝑣𝑜𝑐 𝑎𝑛𝑔𝑙𝑒 −360 ≤ 𝑎𝑛𝑔𝑙𝑒 𝑎𝑛𝑔𝑙𝑒 ≤ 360 𝑐 ≤ 0.5 𝑐 ≥ 0.5 ℎ𝑎𝑣𝑜𝑐 𝑐𝑟𝑜𝑠𝑠𝐶ℎ𝑒𝑐𝑘 −360 ≤ 𝑐𝑟𝑜𝑠𝑠𝐶ℎ𝑒𝑐𝑘 𝑐𝑟𝑜𝑠𝑠𝐶ℎ𝑒𝑐𝑘 ≤ 360 𝑐𝑟𝑜𝑠𝑠𝐶ℎ𝑒𝑐𝑘 == 𝑎𝑛𝑔𝑙𝑒 𝑟𝑒𝑠𝑒𝑡(𝑐) ℎ𝑎𝑣𝑜𝑐 𝑐𝑟𝑜𝑠𝑠𝐶ℎ𝑒𝑐𝑘 −360 ≤ 𝑐𝑟𝑜𝑠𝑠𝐶ℎ𝑒𝑐𝑘 𝑐𝑟𝑜𝑠𝑠𝐶ℎ𝑒𝑐𝑘 ≤ 360 𝑐𝑟𝑜𝑠𝑠𝐶ℎ𝑒𝑐𝑘 ! = 𝑎𝑛𝑔𝑙𝑒 𝑎𝑛𝑔𝑙𝑒 ≔ 0 𝑐𝑟𝑜𝑠𝑠𝐶ℎ𝑒𝑐𝑘 ≔ 0 32
33. Combining CEGAR and Lazy Abstraction for Verifying Timed Systems Combining CEGAR and Lazy Abstraction Precision: 𝜋 = 𝑝 𝑝 = 𝑐𝑟𝑜𝑠𝑠𝐶ℎ𝑒𝑐𝑘 == 𝑎𝑛𝑔𝑙𝑒 Loc. measure 𝑝 C. 𝑐 ≥ 0 ∧ 𝑐 ≤ 0.15 A. 𝑐 ≥ 0    Loc. check 𝑝 C. 𝑐 > 0.05 ∧ 𝑐 ≤ 0.5 A. 𝑐 ≥ 0    Loc. check ¬𝑝 C. 𝑐 > 0.05 ∧ 𝑐 ≤ 0.5 A. 𝑐 ≥ 0    Loc. measure 𝑝 C. 𝑐 ≥ 0 ∧ 𝑐 ≤ 0.15 A. 𝑐 ≥ 0    Running example: simplified model of redundant automotive sensor measure error check timeout 𝑐 ≤ 0.15 c > 0.05 ℎ𝑎𝑣𝑜𝑐 𝑎𝑛𝑔𝑙𝑒 −360 ≤ 𝑎𝑛𝑔𝑙𝑒 𝑎𝑛𝑔𝑙𝑒 ≤ 360 𝑐 ≤ 0.5 𝑐 ≥ 0.5 ℎ𝑎𝑣𝑜𝑐 𝑐𝑟𝑜𝑠𝑠𝐶ℎ𝑒𝑐𝑘 −360 ≤ 𝑐𝑟𝑜𝑠𝑠𝐶ℎ𝑒𝑐𝑘 𝑐𝑟𝑜𝑠𝑠𝐶ℎ𝑒𝑐𝑘 ≤ 360 𝑐𝑟𝑜𝑠𝑠𝐶ℎ𝑒𝑐𝑘 == 𝑎𝑛𝑔𝑙𝑒 𝑟𝑒𝑠𝑒𝑡(𝑐) ℎ𝑎𝑣𝑜𝑐 𝑐𝑟𝑜𝑠𝑠𝐶ℎ𝑒𝑐𝑘 −360 ≤ 𝑐𝑟𝑜𝑠𝑠𝐶ℎ𝑒𝑐𝑘 𝑐𝑟𝑜𝑠𝑠𝐶ℎ𝑒𝑐𝑘 ≤ 360 𝑐𝑟𝑜𝑠𝑠𝐶ℎ𝑒𝑐𝑘 ! = 𝑎𝑛𝑔𝑙𝑒 𝑎𝑛𝑔𝑙𝑒 ≔ 0 𝑐𝑟𝑜𝑠𝑠𝐶ℎ𝑒𝑐𝑘 ≔ 0 33
34. Combining CEGAR and Lazy Abstraction for Verifying Timed Systems Combining CEGAR and Lazy Abstraction Precision: 𝜋 = 𝑝 𝑝 = 𝑐𝑟𝑜𝑠𝑠𝐶ℎ𝑒𝑐𝑘 == 𝑎𝑛𝑔𝑙𝑒 Loc. measure 𝑝 C. 𝑐 ≥ 0 ∧ 𝑐 ≤ 0.15 A. 𝑐 ≥ 0    Loc. check 𝑝 C. 𝑐 > 0.05 ∧ 𝑐 ≤ 0.5 A. 𝑐 ≥ 0    Loc. check ¬𝑝 C. 𝑐 > 0.05 ∧ 𝑐 ≤ 0.5 A. 𝑐 ≥ 0    Loc. measure 𝑝 C. 𝑐 ≥ 0 ∧ 𝑐 ≤ 0.15 A. 𝑐 ≥ 0    Loc. error ¬𝑝 C. 𝑐 > 0.05 A. 𝑐 ≥ 0    Refiner Running example: simplified model of redundant automotive sensor measure error check timeout 𝑐 ≤ 0.15 c > 0.05 ℎ𝑎𝑣𝑜𝑐 𝑎𝑛𝑔𝑙𝑒 −360 ≤ 𝑎𝑛𝑔𝑙𝑒 𝑎𝑛𝑔𝑙𝑒 ≤ 360 𝑐 ≤ 0.5 𝑐 ≥ 0.5 ℎ𝑎𝑣𝑜𝑐 𝑐𝑟𝑜𝑠𝑠𝐶ℎ𝑒𝑐𝑘 −360 ≤ 𝑐𝑟𝑜𝑠𝑠𝐶ℎ𝑒𝑐𝑘 𝑐𝑟𝑜𝑠𝑠𝐶ℎ𝑒𝑐𝑘 ≤ 360 𝑐𝑟𝑜𝑠𝑠𝐶ℎ𝑒𝑐𝑘 == 𝑎𝑛𝑔𝑙𝑒 𝑟𝑒𝑠𝑒𝑡(𝑐) ℎ𝑎𝑣𝑜𝑐 𝑐𝑟𝑜𝑠𝑠𝐶ℎ𝑒𝑐𝑘 −360 ≤ 𝑐𝑟𝑜𝑠𝑠𝐶ℎ𝑒𝑐𝑘 𝑐𝑟𝑜𝑠𝑠𝐶ℎ𝑒𝑐𝑘 ≤ 360 𝑐𝑟𝑜𝑠𝑠𝐶ℎ𝑒𝑐𝑘 ! = 𝑎𝑛𝑔𝑙𝑒 𝑎𝑛𝑔𝑙𝑒 ≔ 0 𝑐𝑟𝑜𝑠𝑠𝐶ℎ𝑒𝑐𝑘 ≔ 0 34
35. Combining CEGAR and Lazy Abstraction for Verifying Timed Systems 35 • 95 XTA models – Synthetic models – Industrial case studies • Restricted set of data operations – Enables comparison with lazy abstraction (det. and nondet.) and CEGAR Evaluation of the Combined Algorithm 1 10 100 0 10 20 30 40 50 60 Time (s) Models verified Lazy abstraction (nondet. supported) Lazy abstraction (deterministic only) Combined algorithm CEGAR The best among configurations with the same expressive power Less expressive power Sensor data User input
36. Combining CEGAR and Lazy Abstraction for Verifying Timed Systems 36 Summary Refiner 🗸 ✗ Abstract counterexample Refined precision Initial precision Abstractor ARG build prune 🗸 ✗ Abstract counterexample Refiner Refined data precision Initial data precision Abstractor Lazy Time Abstractor Lazy Time Refiner Eager Data Abstractor Eager Data Refiner ARG   build prune  🗸 ✗ Lazy Abstractor ARG build Refinement Abstraction