Formal Verification of Probabilistic SystemC Models with Statistical Model Checking

TL;DR

This paper presents a framework and implementation for applying Statistical Model Checking to large, probabilistic SystemC models, enabling efficient property verification without state space explosion.

Contribution

It introduces a novel framework for verifying probabilistic SystemC models using SMC, supporting timed, probabilistic, and user-defined properties with an automated tool.

Findings

Successful verification of large SystemC models using SMC

Support for user-defined primitives and fine-grained timing

Automated instrumentation and trace generation for SMC

Abstract

Transaction-level modeling with SystemC has been very successful in describing the behavior of embedded systems by providing high-level executable models, in which many of them have inherent probabilistic behaviors, e.g., random data and unreliable components. It thus is crucial to have both quantitative and qualitative analysis of the probabilities of system properties. Such analysis can be conducted by constructing a formal model of the system under verification and using Probabilistic Model Checking (PMC). However, this method is infeasible for large systems, due to the state space explosion. In this article, we demonstrate the successful use of Statistical Model Checking (SMC) to carry out such analysis directly from large SystemC models and allow designers to express a wide range of useful properties. The first contribution of this work is a framework to verify properties expressed in Bounded Linear Temporal Logic (BLTL) for SystemC models with both timed and probabilistic characteristics. Second, the framework allows users to expose a rich set of user-code primitives as atomic propositions in BLTL. Moreover, users can define their own fine-grained time resolution rather than the boundary of clock cycles in the SystemC simulation. The third contribution is an implementation of a statistical model checker. It contains an automatic monitor generation for producing execution traces of the model-under-verification (MUV), the mechanism for automatically instrumenting the MUV, and the interaction with statistical model checking algorithms.