Combining CEGAR and Lazy Abstraction for Verifying Timed Systems

Transcript

1. Combining CEGAR
   and Lazy Abstraction
   for Verifying Timed Systems
   Dóra Cziborová
   Alpine Verification Meeting 2023
   

   View Slide

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
   

   View Slide

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
   

   View Slide

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
   

   View Slide

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
   

   View Slide

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
   

   View Slide

7. Combining CEGAR and Lazy Abstraction for Verifying Timed Systems 7
   Abstract Domains
   Zone abstraction
   Explicit value abstraction
   Predicate abstraction
   

   View Slide

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
   

   View Slide

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
   

   View Slide

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
    

    View Slide

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
    𝜋 = 𝑝, 𝑞
    

    View Slide

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
    𝜋 = 𝑝, 𝑞
    

    View Slide

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
    𝜋′ = 𝑝, 𝑞, 𝑟
    𝜋 = 𝑝, 𝑞
    

    View Slide

14. 14
    Lazy Abstraction
    🗸 ✗
    Lazy
    Abstractor
    ARG
    build
    Refinement
    Abstraction
    Combining CEGAR and Lazy Abstraction for Verifying Timed Systems
    

    View Slide

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
    

    View Slide

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
    

    View Slide

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
    

    View Slide

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
    

    View Slide

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
    

    View Slide

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
    

    View Slide

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
    

    View Slide

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
    

    View Slide

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
    

    View Slide

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
    

    View Slide

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
    
    

    View Slide

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
    

    View Slide

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
    

    View Slide

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
    

    View Slide

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
    

    View Slide

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
    

    View Slide

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
    

    View Slide

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
    

    View Slide

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
    

    View Slide

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
    

    View Slide

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
    

    View Slide

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
    

    View Slide