Steady-state property verification: a comparison study

Model checking of probabilistic models can be done either by numerical analysis or by simulation and statistical methods. In this paper, we compare the efficiency and the scalability of different model checking approaches when they are applied to the verification of steady-state properties of large models. We provide an experimental comparison study between the statistical model checking using perfect sampling implemented in Ψ 2 [15] and proposed in [11, 10] and the numerical method implemented in PRISM [6], for the verification of CSL [2] steady-state properties. We show that the proposed statistical approach lets us to consider very large models.

Content

Author and article information

Contributors

Diana El Rabih

Nihal Pekergin

Gaël Gorgo

Jean-Marc Vincent

Conference

Publication date: July 2010

Publication date (Print): July 2010

Pages: 1-12

Affiliations

[0001]LACL

University of Paris-Est Créteil- Val de Marne,

61 avenue Général de Gaulle 94010, Créteil, France

[0002]LIG

University of Grenoble, 51, av. Jean Kuntzmann,

38330 MONTBONNOT, France

Article

DOI: 10.14236/ewic/VECOS2010.12

SO-VID: 020556cf-a33a-4cab-8fb6-aa0f83e589bb

Copyright statement: © Diana El Rabih et al. Published by BCS Learning and Development Ltd. Fourth International Workshop on Verification and Evaluation of Computer and Communication Systems (VECoS 2010), Paris, France

License:

This work is licensed under a Creative Commons Attribution 4.0 Unported License. To view a copy of this license, visit http://creativecommons.org/licenses/by/4.0/

Conference name: Fourth International Workshop on Verification and Evaluation of Computer and Communication Systems (VECoS 2010)

Conference acronym: VECOS

Conference number: 4

Conference location: Paris, France

Conference date: 1-2 July 2010

Conference sponsor: Electronic Workshops in Computing (eWiC)

Conference theme: Verification and Evaluation of Computer and Communication Systems (VECoS 2010)

Product

Product Information: 1477-9358BCS Learning & Development

Self URI (article page): https://www.scienceopen.com/hosted-document?doi=10.14236/ewic/VECOS2010.12

Self URI (journal page): https://ewic.bcs.org/

Steady-state property verification: a comparison study

Abstract