UPPAAL SMC

UPPAAL SMC

Description: Statistical Model Checking (SMC) refers to a series of techniques that monitor several runs of the system with respect to some property, and then use results from the statistics to get an overall estimate of the correctness of the design. The approach has been applied to problems that are far beyond the scope of existing model checkers. In fact, SMC gets widely accepted in various research areas such as systems biology [JCLLPZ09, CFLHJL08] or software engineering [You05a], in particular for industrial applications [BBBCDL10]. There are several reasons for this success. First, it is very simple to implement, understand and use (especially by industry, software engineers, and generally all people that are not pure researchers but customers for our results and tools). Second, it requires little or no extra modeling or specification effort, but simply an operational model of the system that can be simulated and checked against properties. Third, the use of Statistics allows to approximate undecidable problems. Finally, it is possible to easily distribute SMC [BDLLMP12].

VO Integration: No

Active: No

Available Benchmarks: No

Website: http://people.cs.aau.dk/~adavid/smc/

Download: Main UPPAAL release.

Documentation: Case studies and example.

Contact: Link to list of contributors.

Excerpt from: http://people.cs.aau.dk/~adavid/smc/