Probabilistic model checking of systems with ranged probabilities
View Patent ↗Systems and methods for model checking of live systems are shown that include learning an interval discrete-time Markov chain (IDTMC) model of a deployed system from system logs; and checking the IDTMC model with a processor to determine a probability of violating one or more probabilistic safety properties. Checking the IDTMC model includes calculating a linear part exactly using affine arithmetic; and over-approximating a non-linear part using interval arithmetic.
1. A method for model checking of deployed systems, comprising:
learning an interval discrete-time Markov chain (IDTMC) model of a deployed system from system logs; and
checking the IDTMC model with a processor to determine a probability of violating one or more probabilistic safety properties, comprising:
splitting the probability into a linear part and a non-linear part; and
calculating the linear part exactly using affine arithmetic; and
over-approximating the non-linear part using interval arithmetic.
2. The method of claim 1 , further comprising testing the deployed system to determine whether a given probabilistic safety property is violated based on the probability of violating the given probabilistic safety property.
3. The method of claim 2 , wherein checking the IDTMC model further comprises checking the DTMC model and propagating forward the perturbations.
4. The method of claim 1 , wherein checking the IDTMC model further comprises splitting the IDTMC into a discrete-time Markov chain (DTMC) model and perturbations.
5. The method of claim 1 , wherein checking the IDTMC model further comprises computing interval bounds for the non-linear part using the calculated linear part.
6. The method of claim 5 , wherein computing interval bounds for the non-linear part comprises solving a set of linear programming problems.
7. The method of claim 6 , wherein computing interval bounds for the non-linear part comprises reformulating the set of linear programming problems as a weighted median problem.
8. The method of claim 1 , wherein the one or more probabilistic safety properties include a bounded property.
9. The method of claim 1 , wherein the one or more probabilistic safety properties include an unbounded property.
10. A system for model checking of deployed systems, comprising:
a model learning module configured to learn an interval discrete-time Markov chain (IDTMC) model of a deployed system from system logs; and
a processor configured to check the IDTMC model to determine a probability of violating one or more probabilistic safety properties, wherein the probability is split into a linear part and a non-linear part, comprising:
an affine module configured to calculate a linear part exactly using affine arithmetic; and
an interval module configured to over-approximate a non-linear part using interval arithmetic.