The Statistical Model-Checking

The most common method used in industry to ensure the correctness of a system with respect to some specification is testing. After the computer system is constructed, it is tested using a number of test cases with predicted outcomes. Testing techniques have shown effectiveness in bug hunting in many industrial problems. Unfortunately, testing is not a panacea. Indeed.

Since there is, in general, no way for a finite set of test cases to cover all possible scenarios, errors may remain undetected.

Moreover, quantitative aspects are mostly ignored (there is almost no techniques for testing stochastic systems).

Dynamism is hardly handled as testing works together with stimuli, but without a clever technique to monitor programs' executions.

There are also methods that can ensure the full correctness of a system. Those methods, also called formal methods, use mathematical techniques to check whether the system will behave correctly for all possible scenarios. Over the past, formal methods such as symbolic model checking have been used to verify systems with more than 10^{20}reachable states.

In an ideal world, it would thus be "better'' to use formal methods rather than testing ones. Unfortunately, aside from the fact that dynamicity is hardly handled (especially in the stochastic case), improvements in development of formal methods do not seem to follow the increasing complexity in system design. Nowadays, most of formal methods suffer from the so-called state-space explosion problem, which makes them unenforceable to large industrial case studies (but those techniques fit perfectly for punctual problems). As testing does not suffer from the same problem, it remains the only scalable technique and it is thus the one promoted by the industrials.

As we already said, the major drawback with testing is that, in general, it does not give any confidence on the correctness of the entire system. This lack of accuracy has motivated the development of new algorithms that combine testing techniques with algorithms coming from the statistical area. Those techniques, also called Statistical Model Checking techniques (SMC), can be seen as a trade-off between testing and formal verification. The core idea of the approach is to conduct some simulations of the system and verify if they satisfy some given property. The results are then used together with algorithms from the statistical area in order to decide whether the system satisfies the property with some probability.

Statistical model checking techniques can also be used to estimate the probability that a system satisfies a given property. Of course, in contrast with an exhaustive approach, a simulation-based solution does not guarantee a result with 100% confidence. However, it is possible to bound the probability of making an error. Simulation-based methods are known to be far less memory and time intensive than exhaustive ones, and are sometimes the only option. Statistical model checking gets widely accepted in various research areas such as software engineering, in particular for industrial applications, or even for solving problems originating from systems biology. There are several reasons for this success:

  1. SMC is very simple to understand, implement, and use.
  2. It does not require extra modeling or specification effort, but simply an operational model of the system, that can be simulated and checked against state-based properties.
  3. It allows to verify properties that cannot be expressed in classical temporal logics.
  4. It allows to reason quantitatively on the correctness of the system.
  5. Finally, contrary to other techniques, the use of “clever” monitors could help to handle dynamicity.

The Statistical Model Checking applied to SoS.
In DANSE, we adapt the SMC techniques to treat large heterogeneous systems like Systems of Systems. Among them, one finds systems integrating multiple heterogeneous distributed applications communicating over a shared network. Those applications, also called heterogeneous systems are typical in various sensitive domains such as aeronautic or automotive embedded systems. We propose to extend UPDM specification – the SoS specification – with some requirements that the implemented strategies over the SoS must satisfy. These requirements, also called contracts, are specified with a new contract language specially designed for the SoS's.

These goals are viewed as behavioral objectives that lead the system architect for implementing some good strategies in the SoS. These contracts are in high-level English-pattern language but have an accurate semantics given by the standard temporal logics. These contracts are verified against the UPDM specification is compiled into a FMI executable system using the Statistical Model Checker PLASMA (INRIA) combined with the simulation engine DESYRE (Ales) : the SMC tool-chain gives an estimation of the satisfiability of the contract by the SoS. The different helps the system architect to select what are the best strategies and optimizations to implement in the SoS.

Home DANSE The Statistical Model-Checking