Statistical Model Checking for Priced Timed Automata

被引：26

作者：

Bulychev, Peter ^{[1
]}

David, Alexandre ^{[1
]}

Larsen, Kim Guldstrand ^{[1
]}

Legay, Axel ^{[2
,3
]}

Mikucionis, Marius ^{[1
]}

Poulsen, Danny Bogsted ^{[1
]}

Wang, Zheng ^{[4
]}

机构：

[1] Aalborg Univ, Dept Comp Sci, Aalborg, Denmark

[2] INRIA, Rennes, France

[3] Aalborg Univ, Dept Comp Sci, Aalborg, Denmark

[4] East China Normal Univ, Software Engn Inst, Shanghai Key Lab Trustworthy Comp, Shanghai, Peoples R China

来源：

ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE | 2012年 / 85期

关键词：

D O I：

10.4204/EPTCS.85.1

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

This paper offers a survey of UPPAAL-SMC, a major extension of the real-time verification tool UPPAAL. UPPAAL-SMC allows for the efficient analysis of performance properties of networks of priced timed automata under a natural stochastic semantics. In particular, UPPAAL-SMC relies on a series of extensions of the statistical model checking approach generalized to handle real-time systems and estimate undecidable problems. UPPAAL-SMC comes together with a friendly user interface that allows a user to specify complex problems in an efficient manner as well as to get feedback in the form of probability distributions and compare probabilities to analyze performance aspects of systems. The focus of the survey is on the evolution of the tool - including modeling and specification formalisms as well as techniques applied - together with applications of the tool to case studies.

引用

页码：1 / 16

页数：16

共 38 条

[1] THE ALGORITHMIC ANALYSIS OF HYBRID SYSTEMS [J].

ALUR, R ;

COURCOUBETIS, C ;

HALBWACHS, N ;

HENZINGER, TA ;

HO, PH ;

NICOLLIN, X ;

OLIVERO, A ;

SIFAKIS, J ;

YOVINE, S .

THEORETICAL COMPUTER SCIENCE, 1995, 138 (01) :3-34

[2] Model-checking algorithms for continuous-time Markov chains [J].

Baier, C ;

Haverkort, B ;

Hermanns, H ;

Katoen, JP .

IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 2003, 29 (06) :524-541

[3]

Barbot B, 2011, LECT NOTES COMPUT SC, V6605, P128, DOI 10.1007/978-3-642-19835-9_12

[4]

Basu A, 2010, LECT NOTES COMPUT SC, V6117, P32, DOI 10.1007/978-3-642-13464-7_4

[5]

Behrmann G., 2001, Hybrid Systems: Computation and Control. 4th International Workshop, HSCC 2001. Proceedings (Lecture Notes in Computer Science Vol.2034), P147

[6]

Behrmann G., 2007, LNCS, V4590

[7]

Bouyer P, 2010, HSSC 10: PROCEEDINGS OF THE 13TH ACM INTERNATIONAL CONFERENCE ON HYBRID SYSTEMS: COMPUTATION AND CONTROL, P61

[8]

Bulychev Peter, 2012, NASA Formal Methods. Proceedings of the 4th International Symposium, NFM 2012, P449, DOI 10.1007/978-3-642-28891-3_39

[9]

Bulychev P, 2011, ELECTRON P THEOR COM, P30, DOI 10.4204/EPTCS.72.4

[10] Computing Nash Equilibrium in Wireless Ad Hoc Networks: A Simulation-Based Approach [J].

Bulychev, Peter ;

David, Alexandre ;

Larsen, Kim G. ;

Legay, Axel ;

Mikucionis, Marius .

ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2012, (78) :1-14

← 1 2 3 4 →