Simulation-Based Model Checking for Nondeterministic Systems and Rare Events
Abstract
Objective: This project extends statistical model checking methods to enable reasoning about nondeterministic systems and extremely rare events. Approach: To address nondeterministic systems, we investigated a theoretical framework integrating semi-exhaustive simulation with hierarchical abstraction of models. For rare events, we investigated importance sampling methods that rely on variance minimization and cross- entropy methods to optimize biasing distributions, allowing statistical methods to reason accurately about low-probability events. Outcome/Impact: Statistical model checking methods scale better than traditional analytic methods for very large systems; this research is critical to allow statistical methods to reason about realistic systems involving nondeterminism and low-probability events. Our new methods will be implemented in the PRISMATIC tool, supporting testing, evaluation, and eventually application to verification of real-world systems.
Document Details
- Document Type
- Technical Report
- Publication Date
- Mar 24, 2016
- Accession Number
- AD1010702
Entities
People
- David Musliner
- Edmund M. Clarke
- Qinsi Wang
- Robert P. Goldman
- Soonho Kong
Organizations
- Carnegie Mellon University