Upgrade to Pro — share decks privately, control downloads, hide ads and more …

Combining CEGAR and Lazy Abstraction for Verify...

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.

Critical Systems Research Group

September 26, 2023
Tweet

More Decks by Critical Systems Research Group

Other Decks in Research

Transcript

  1. 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
  2. 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
  3. 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
  4. 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
  5. 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
  6. Combining CEGAR and Lazy Abstraction for Verifying Timed Systems 7

    Abstract Domains Zone abstraction Explicit value abstraction Predicate abstraction
  7. 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
  8. 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
  9. 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
  10. 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 𝜋 = 𝑝, 𝑞
  11. 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 𝜋 = 𝑝, 𝑞
  12. 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 𝜋′ = 𝑝, 𝑞, 𝑟 𝜋 = 𝑝, 𝑞
  13. 14 Lazy Abstraction 🗸 ✗ Lazy Abstractor ARG build Refinement

    Abstraction Combining CEGAR and Lazy Abstraction for Verifying Timed Systems
  14. 15 Lazy Abstraction Nodes with concrete and abstract labels 🗸

    ✗ Lazy Abstractor ARG build Refinement Abstraction Combining CEGAR and Lazy Abstraction for Verifying Timed Systems
  15. 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
  16. 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
  17. 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
  18. 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
  19. 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
  20. 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
  21. 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
  22. 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
  23. 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
  24. 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 
  25. 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
  26. 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
  27. 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
  28. 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
  29. 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
  30. 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
  31. 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
  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    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
  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    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
  34. 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
  35. 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