A STORM is Coming: A Modern Probabilistic Model Checker

被引：282

作者：

Dehnert, Christian ^{[1
]}

Junges, Sebastian ^{[1
]}

Katoen, Joost-Pieter ^{[1
]}

Volk, Matthias ^{[1
]}

机构：

[1] Rhein Westfal TH Aachen, Aachen, Germany

来源：

COMPUTER AIDED VERIFICATION (CAV 2017), PT II | 2017年 / 10427卷

关键词：

PARAMETER SYNTHESIS;

D O I：

10.1007/978-3-319-63390-9_31

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

We launch the new probabilistic model checker Storm. It features the analysis of discrete- and continuous-time variants of both Markov chains and MDPs. It supports the Prism and JANI modeling languages, probabilistic programs, dynamic fault trees and generalized stochastic Petri nets. It has a modular set-up in which solvers and symbolic engines can easily be exchanged. It offers a Python API for rapid prototyping by encapsulating Storm's fast and scalable algorithms. Experiments on a variety of benchmarks show its competitive performance.

引用

页码：592 / 600

页数：9

共 42 条

[1]

Abraham Erika, 2014, Formal Methods for Executable Software Models. 14th International School on Formal Methods for the Design of Computer, Communication, and Software Systems, SFM 2014. Advanced Lectures: LNCS 8483, P65, DOI 10.1007/978-3-319-07317-0_3

[2]

Aljazzar Husain, 2011, Model Checking Software. Proceedings 18th International SPIN Workshop, P183, DOI 10.1007/978-3-642-22306-8_13

[3]

Amparore Elvio Gilberto, 2014, Application and Theory of Petri Nets and Concurrency. 35th International Conference, PETRI NETS 2014. Proceedings: LNCS 8489, P354, DOI 10.1007/978-3-319-07734-5_19

[4]

[Anonymous], 2014, PROC FOSE 14, DOI DOI 10.1145/2593882.2593900

[5]

[Anonymous], LECT NOTES COMPUTER

[6] 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

[7]

Baier C, 2014, LNCS, V8413, P515, DOI DOI 10.1007/978-3-642-54862-8

[8] A Rigorous, Compositional, and Extensible Framework for Dynamic Fault Tree Analysis [J].

Boudali, Hichem ;

Crouzen, Pepijn ;

Stoelinga, Marielle .

IEEE TRANSACTIONS ON DEPENDABLE AND SECURE COMPUTING, 2010, 7 (02) :128-143

[9]

Brázdil T, 2014, LECT NOTES COMPUT SC, V8837, P98, DOI 10.1007/978-3-319-11936-6_8

[10] JANI: Quantitative Model and Tool Interaction [J].

Budde, Carlos E. ;

Dehnert, Christian ;

Hahn, Ernst Moritz ;

Hartmanns, Arnd ;

Junges, Sebastian ;

Turrini, Andrea .

TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, TACAS 2017, PT II, 2017, 10206 :151-168

← 1 2 3 4 5 →