PSCV is a tool for verifying probabilistic properties of a class of SystemC models which have inherent probabilistic characteristics. The tool accepts input properties of the forms Pr(p), Pr >= a (p), and X <= T (rv), where p is a temporal property expressed using the Bounded Linear Temporal Logic (BLTL). The former is used to compute the probability that p satisfied by the model. The later asserts that this probability is at least equal to the threshold a. The last one returns the mean value of the random variable rv within T time units of execution.

PSCV is a free software under GNU GPL Version 3 license for its original components. Click the links below to read and accept the licenses for downloading other components. It consists of off-the-self, modified and original components:

• An off-the-self component, AspectC++ from aspectc.org, a C++ aspect compiler that is used for instrumenting the model under verifying
• A modified component, a patch version of SystemC-2.3.0 from Accellera, to facilitate the communication between the kernel and the monitor and implement a random scheduler for the kernel
• Two original components are MAG, a C++ tool for automatically generating monitor and aspect advices from properties of interest for instrumentation, and SystemC plugin, a plugin of the statistical model checker Plasma Lab from INRIA used for checking the satisfaction and computing probabilities of probabilistic temporal properties