Time for Statistical Model Checking of Real-Time Systems

A. David; Kim Guldstrand Larsen; A. Legay; Marius Mikucionis; Z. Wang

doi:10.1007/978-3-642-22110-1_27

Time for Statistical Model Checking of Real-Time Systems

A. David, Kim Guldstrand Larsen, A. Legay, Marius Mikucionis, Z. Wang

Research output: Contribution to journal › Conference article in Journal › Research › peer-review

113 Citations (Scopus)

Abstract

We propose the first tool for solving complex (some undecidable) problems of timed systems by using Statistical Model Checking (SMC). The tool monitors several runs of the system, and then relies on statistical algorithms to get an estimate of the correctness of the entire design. Contrary to other existing toolsets, ours relies on i) a natural stochastic semantics for networks of timed systems, ii) an engine capable to solve problems that are beyond the scope of classical model checkers, and iii) a friendly user interface.

Original language	English
Book series	Lecture Notes in Computer Science
Volume	6806 LNCS
Pages (from-to)	349-355
Number of pages	7
ISSN	0302-9743
DOIs	https://doi.org/10.1007/978-3-642-22110-1_27
Publication status	Published - 1 Jan 2011
Event	23rd International Conference on Computer Aided Verification - Snowbird, UT, United States Duration: 14 Jul 2011 → 20 Jul 2011 Conference number: 23

Conference

Conference	23rd International Conference on Computer Aided Verification
Number	23
Country/Territory	United States
City	Snowbird, UT
Period	14/07/2011 → 20/07/2011

Access to Document

10.1007/978-3-642-22110-1_27

AUB Link

Search for the material in Aalborg University Library's search engine

Cite this

@inproceedings{dc8ad9e50ce54581a53122888209381a,

title = "Time for Statistical Model Checking of Real-Time Systems",

abstract = "We propose the first tool for solving complex (some undecidable) problems of timed systems by using Statistical Model Checking (SMC). The tool monitors several runs of the system, and then relies on statistical algorithms to get an estimate of the correctness of the entire design. Contrary to other existing toolsets, ours relies on i) a natural stochastic semantics for networks of timed systems, ii) an engine capable to solve problems that are beyond the scope of classical model checkers, and iii) a friendly user interface.",

author = "A. David and Larsen, {Kim Guldstrand} and A. Legay and Marius Mikucionis and Z. Wang",

note = "Proceedings of the 23rd International Conference on Computer Aided Verification. Gopalakrishnan, G. & Qadeer, S. (eds.); 23rd International Conference on Computer Aided Verification ; Conference date: 14-07-2011 Through 20-07-2011",

year = "2011",

month = jan,

day = "1",

doi = "10.1007/978-3-642-22110-1_27",

language = "English",

volume = "6806 LNCS",

pages = "349--355",

journal = "Lecture Notes in Computer Science",

issn = "0302-9743",

publisher = "Physica-Verlag",

}

TY - GEN

T1 - Time for Statistical Model Checking of Real-Time Systems

AU - David, A.

AU - Larsen, Kim Guldstrand

AU - Legay, A.

AU - Mikucionis, Marius

AU - Wang, Z.

N1 - Conference code: 23

PY - 2011/1/1

Y1 - 2011/1/1

N2 - We propose the first tool for solving complex (some undecidable) problems of timed systems by using Statistical Model Checking (SMC). The tool monitors several runs of the system, and then relies on statistical algorithms to get an estimate of the correctness of the entire design. Contrary to other existing toolsets, ours relies on i) a natural stochastic semantics for networks of timed systems, ii) an engine capable to solve problems that are beyond the scope of classical model checkers, and iii) a friendly user interface.

AB - We propose the first tool for solving complex (some undecidable) problems of timed systems by using Statistical Model Checking (SMC). The tool monitors several runs of the system, and then relies on statistical algorithms to get an estimate of the correctness of the entire design. Contrary to other existing toolsets, ours relies on i) a natural stochastic semantics for networks of timed systems, ii) an engine capable to solve problems that are beyond the scope of classical model checkers, and iii) a friendly user interface.

UR - http://www.scopus.com/inward/record.url?scp=79960376940&partnerID=8YFLogxK

U2 - 10.1007/978-3-642-22110-1_27

DO - 10.1007/978-3-642-22110-1_27

M3 - Conference article in Journal

AN - SCOPUS:79960376940

SN - 0302-9743

VL - 6806 LNCS

SP - 349

EP - 355

JO - Lecture Notes in Computer Science

JF - Lecture Notes in Computer Science

T2 - 23rd International Conference on Computer Aided Verification

Y2 - 14 July 2011 through 20 July 2011

ER -

Time for Statistical Model Checking of Real-Time Systems

Abstract

Conference

Access to Document

AUB Link

Other files and links

Fingerprint

Cite this