Dynamic Verification of SystemC with Statistical Model Checking
This work addresses the verification of probabilistic and temporal properties in large, realistic embedded systems, which is incremental as it builds on existing statistical model checking techniques.
The authors tackled the state space explosion problem in probabilistic model checking for realistic embedded and real-time systems by proposing a verification framework based on Statistical Model Checking, which is fully implemented as an extension of the Plasma-lab tool and demonstrated on a multi-lift system case study.
Many embedded and real-time systems have a inherent probabilistic behaviour (sensors data, unreliable hardware,...). In that context, it is crucial to evaluate system properties such as "the probability that a particular hardware fails". Such properties can be evaluated by using probabilistic model checking. However, this technique fails on models representing realistic embedded and real-time systems because of the state space explosion. To overcome this problem, we propose a verification framework based on Statistical Model Checking. Our framework is able to evaluate probabilistic and temporal properties on large systems modelled in SystemC, a standard system-level modelling language. It is fully implemented as an extension of the Plasma-lab statistical model checker. We illustrate our approach on a multi-lift system case study.