Abstract | ||
---|---|---|
Statistical Model Checking (SMC) is a trade-off between testing and formal verification. The core idea of the approach is to conduct some simulations of the system and verify if they satisfy some given property. In this paper we show that SMC is easily parallelizable on amaster/slaves architecture by introducing a series of algorithms that scale almost linearly with respect to the number of slave computers. Our approach has been implemented in the UPPAAL SMC toolset and applied on nontrivial case studies. |
Year | DOI | Venue |
---|---|---|
2011 | 10.4204/EPTCS.72.4 | ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE |
Keywords | Field | DocType |
statistical model,satisfiability,software engineering,formal verification,cluster computing | Parallelizable manifold,Architecture,Computer science,Statistical model checking,Theoretical computer science,Parametric statistics,Formal verification | Journal |
Issue | ISSN | Citations |
72 | 2075-2180 | 4 |
PageRank | References | Authors |
0.43 | 8 | 5 |
Name | Order | Citations | PageRank |
---|---|---|---|
Peter Bulychev | 1 | 79 | 3.97 |
Alexandre David | 2 | 1667 | 76.52 |
Kim Guldstrand Larsen | 3 | 4434 | 346.88 |
Marius Mikučionis | 4 | 799 | 33.52 |
Axel Legay | 5 | 2982 | 181.47 |