PV3 ⊧ STMC: Statistical Model Checkercan verify any property expressible in PRISM against any system expresible in PRISM

Statistical model checker. "[STMC can] statically verify any black-box probabilistic system that PRISM can simulate, against probabilistic bounds on any property that PRISM can evaluate over individual executions of the system."

Application domain/field

• Model checking
• Statistical model checking

Type of tool

Statistical model checker

Expected input

Probabilistic model

Format:

PRISM (.pm file)

Expected output

? ("Result: true" or "Result: false"?)

Internals

Uses PRISM

Comments

License: GNU General Public License v3.0