TY - JOUR
T1 - Statistical model checking
T2 - Challenges and perspectives
AU - Legay, Axel
AU - Viswanathan, Mahesh
N1 - Publisher Copyright:
© Springer-Verlag London 2015.
PY - 2015/8/1
Y1 - 2015/8/1
N2 - Statistical model checking (SMC) is a powerful and widely used approach that consists in estimating the probability for a system to satisfy a temporal property. This is done by monitoring a finite number of executions of the system, and then extrapolating the result using statistics. The answer is correct up to some confidence that can be parameterized by the user. It is known that SMC mitigates the state-space explosion problem and allows us to handle requirements that cannot be expressed in classical temporal logics. The approach has been implemented in several toolsets, and successfully applied in a wide range of diverse areas such as systems biology, robotic, or automotive. The objectives of this special issue are (1) to survey existing results on SMC, (2) to propose SMC algorithms for a larger class of systems, and (3) to show the applicability of SMC to new emerging applications.
AB - Statistical model checking (SMC) is a powerful and widely used approach that consists in estimating the probability for a system to satisfy a temporal property. This is done by monitoring a finite number of executions of the system, and then extrapolating the result using statistics. The answer is correct up to some confidence that can be parameterized by the user. It is known that SMC mitigates the state-space explosion problem and allows us to handle requirements that cannot be expressed in classical temporal logics. The approach has been implemented in several toolsets, and successfully applied in a wide range of diverse areas such as systems biology, robotic, or automotive. The objectives of this special issue are (1) to survey existing results on SMC, (2) to propose SMC algorithms for a larger class of systems, and (3) to show the applicability of SMC to new emerging applications.
KW - Overview
KW - Quantities statistical model checking
UR - http://www.scopus.com/inward/record.url?scp=84943361423&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84943361423&partnerID=8YFLogxK
U2 - 10.1007/s10009-015-0384-z
DO - 10.1007/s10009-015-0384-z
M3 - Article
AN - SCOPUS:84943361423
SN - 1433-2779
VL - 17
SP - 369
EP - 376
JO - International Journal on Software Tools for Technology Transfer
JF - International Journal on Software Tools for Technology Transfer
IS - 4
M1 - A011
ER -