Probabilistic Model Checking
When we design a new system, an important question that ususally pops up is - How do we ensure dependability and performance of the system ? With recent advances in ubiquitous computing, systems are getting more complicated. Networking and wireless are becoming a more common phenomena across these devices. Systems are becoming context-aware and adaptive. Many suggest a transformation in the conventional software engineering flows and coming up with model-based software engineering and model-based verification techniques.
To rule out errors, one must consider all possible executions in a program, which is often not possible mechanically. Given that computer systems are getting sophisticated, this has become more difficult to achieve. Formal Verification (FV) domain provides us with effective techniques for the same. There are various techniques ranging from manual mathematical proofs to fast, lightweight static analysis methods. We focus on model-checking, that is fully-automatic and exhaustive in terms of state space coverage.
Automatic Model Checking techniques give assurance of a safe, dependable system with a good performance and trust in security and privacy. However we want to discuss probabilistic model checking. We want to capture probability and resource usage in a computer system. Probability is an effective tool to model uncertainty and performance of a system. By doing so, we quantify the rate of failures and express Quality of Service (QoS). It is used in an evidence based statistical analysis of behaviours to quantify terms like trust and anonymity.
Probabilistic Model Checking is an FV technique for modelling and verifying systems that exhibit stochastic behaviour. Three most commonly used probabilistic models are:
- Discrete-Time Markov Chains (DTMC)
- Markov Decision Processes (MDP)
- Continuous-Time Markov Chains (CTMC)