Dynamic Verification of SystemC with Statistical Model Checking

Ngo Van, Chan;Legay, Axel;Quilbeuf, Jean
(2014)

Files

No attached file found for this publication.

Details

Authors
  • Ngo Van, Chan
    Author
  • Legay, AxelUCLouvain
    Author
  • Quilbeuf, Jean
    Author
Abstract
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.

Citations

Ngo Van, C., Legay, A., & Quilbeuf, J. (2014). Dynamic Verification of SystemC with Statistical Model Checking. https://hdl.handle.net/2078.5/173065