- Home
- Documents
*Counterexamples for Timed Reachability Analysis ... 8 Analysis of Stochastic Models Various model...*

prev

next

out of 29

View

0Download

0

Embed Size (px)

Counterexamples for Timed Probabilistic Reachability

Husain Aljazzar Software Engineering

University of Constance

2

Joint work with

Holger Hermanns, Saarland University Stefan Leue, University of Constance

3

Overview

Introduction (Directed) Explicit-State Model Checking (D)ESMC for Timed Probabilistic Reachability Probabilistic Quality Measure for (D)ESMC Case Study and Experimental Results Conclusion & Future Work

4

Overview

Introduction (Directed) Explicit-State Model Checking (D)ESMC for Timed Probabilistic Reachability Probabilistic Quality Measure for (D)ESMC Case Study and Experimental Results Conclusion & Future Work

5

Stochastic Models Stochastic models, e.g. DTMCs and CTMCs: modeling and analysis of system performance and dependability.

communication protocols, embedded systems, etc…

A DTMC is a quadruple (S, s0, P, L), where S is a finite set of states, and s0 ∈ S is an initial state P : S × S → R is the transition probability matrix, L : S → 2AP is labeling function.

6

Stochastic Models

A CTMC is a quintuple (S, s0, P, L, E), where (S, s0, P, L) is a DTMC E: S → R is a function assigning each state an exit rate Exit times are exponentially distributed

E.g. E := {(s0, 3), (s1, 0), (s2, 5)} 3 5

0

7

Runs and Paths In a DTMC, we call a finite/infinite sequence of states finite/infinite RUN

In a CTMC, a finite/infinite PATH is a timed variant of a run in the underlying DTMC.

Infinite branching tree due to varying transition time durations of transitions.

8

Analysis of Stochastic Models Various model checking approaches for stochastic models have been presented. Our point of reference: CSL model checking

Baier, C., Haverkort, B., Hermanns, H., Katoen, J.P. “Model-Checking Algorithms for Continuous-Time Markov chains”

IEEE Transitions on Software Engineering 29, 2003 Continuous Stochastic Logic (CSL): CSL model checking algorithms: efficient, approximate, numerical

Common weakness: Inability to give detailed debugging information (Counterexamples).

Problematic for debugging

Approach: Use explicit state space algorithms to select offending system runs (counterexamples).

9

Timed Probabilistic Reachability Analysis

Timed Reachability Property: The probability to reach a state s violating a state proposition ϑ, i.e., satisfying ϕ := ¬ ϑ, within a given time period t does not exceed a probability bound p.

Specification using Continuous Stochastic Logic (CSL)

P

10

Overview

Introduction (Directed) Explicit-State Model Checking (D)ESMC for Timed Probabilistic Reachability Probabilistic Quality Measure for (D)ESMC Case Study and Experimental Results Conclusion & Future Work

11

What is a Counterexample? (of Timed Probabilistic Reachability)

In non-stochastic models: a counterexample is an offending run. In stochastic models:

DTMC: All offending runs CTMC: The infinite cylinder set containing all paths that reach an error state within the time period t.

A single path of the cylinder set? Runs in the underlying DTMC

A counterexample is an offending run in the (underlying) DTMC.

12

(Directed) Explicit-State Model Checking (D)ESMC

ESMC (DFS)

ESMC (BFS) and DESMC (A*) with path-length as optimizing criterion search we want this!

A mass to measure the quality of runs is required.

13

Overview

14

Timed Run Probability Let r = s0 → s1 → s2 → … → sn be a run. The timed run probability of r in the time period t.

Computation: In CT-case:

In DT-case:

s0 sn

Execution time · t

r =

15

Uniformization Using the uniformization we turn a CTMC A into a DTMC A´ for which we can efficiently compute the timed run probability γ´.

A´ is embedded into a Poisson process which describes the probability that a particular discrete number of events k occurs within a real time period t.

16

Approximation for the Timed Run Probability in CTMC

We denote the expected value of the Poisson process after time period t as N.

We assume that the derived DTMC A´ makes N hops within the time period t.

γ(r, t) (in A) is approximated by γ´(r, N) (in A´), which is much easier to compute.

Our search algorithms use γ´(r, N) as a quality measure for runs of the CTMC (optimizing criterion).

17

Intriguing Example

r2

r1

2

2 0

20 20 0

18

Quality of Uniformization Approximation

r2

r1 2

2 20 20 0

0

Note: the run with optimal timed run probability changes with the time bound t!

Time bound smaller than t r1 is optimal Time bound larger than t

r2 is optimal

19

ESMC and DESMC for Stochastic Models

Now we are able to explore CTMCs (and DTMCs) using optimizing algorithms, and select counterexamples which are approximating the optimal timed run probability values.

Search Algorithms Dijkstra (undirected, ESMC) Directed search algorithms (DESMC)

Z* and Greedy Best First Search (GBestFS) Directed search algorithms use knowledge about

the state space or/and the specification of the goal state

A heuristic function h is used in the state evaluation. Advantages of DESMC: Improving the performance

Memory consumption Runtime

20

Overview

21

Case-Study: SCSI-2-Protocol

In our experiments: One Controller One main disk (frequently used) Two backup disks (rarely used)

LOTOS model Interactive Markov chain (IMC) CTMC

22

SCSI-2-Protocol: A Timed Reachability Property

Main disk overload (MDOL): The main disk is overloaded while the backup disks are not accessed. Timed Reachability Property: The probability to reach a MDOL state within the time period t does not exceed 30%.

A heuristic function based on the status of the disk queues.

23

SCSI-2-Protocol: Counterexample

The counterexample delivered by Z*

24

SCSI-Protocol: Experimental Results For each time bound from 1 to 10:

Probability to violate the property Timed run probability for the counterexamples delivered by the search algorithms.

0

0.05

0.1

0.15

0.2

0.25

0.3

0.35

1 2 3 4 5 6 7 8 9 10

Time bound

Pr ob

ab ili

ty

Model DFS BFS Dijkstra GBestFS Z*

25

SCSI-Protocol: Experimental Results Memory consumption

The behavior of DFS and BFS is unacceptable. Dijkstra is OK but not excellent Z* and GBestFS bring significant improvement GBestFS has the best behavior.

Similar results for runtime

26

Overview

27

Conclusion Counterexamples

defined counterexamples for CTMCs, including their probability mass: timed run probabilities approximate the computationally expensive timed run probabilities through uniformisation

Directed CTMC Exploration use approximative timed run probability in determining generating path costs combine with domain specific information to compute admissible heuristic estimates (admissible in the approximated model)

Experimental Evaluation (SCSI-2) using approximated timed run probabilities allows Dijkstra and heuristic search algorithms to find meaningful counterexamples heuristics guided search is computationally superior to uninformed search

28

Future Work Threats to Valitidy

more experimental data convergence to PRISM tool environment, more models available use randomly generated models

Underapproximation of Timed Probabilistic Reachability find tree of offending system runs so that combined probability mass exceeds probability bound potentially computationally much more efficient than precise solution of problem

Application to Other Stochastic Models Continuous Time Markov Decision Processes

contain non-determinism

29

Thanks for your attention!

Counterexamples for Timed Probabilistic Reachability Joint work with Overview Overview Stochastic Models Stochastic Models Runs and Paths Analysis of Stochastic Models Timed Probabilistic Reachability Analysis Overview What is a Counterexample?(of Timed Probabilistic Reachabilit