Towards light-weight probabilistic model checking

DOI10.1155/2014/814159MaRDI QIDQ2336743zbMATH OpenOpenAlexWikidataFDO

Authors Savas Konur

Publication date 19 November 2019

Published in Journal of Applied Mathematics (Search for Journal in Brave)

Copyright license Creative Commons Attribution 3.0 Unported

Full work available at URL https://doi.org/10.1155/2014/814159

Mathematics Subject Classification ID

Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.) (68Q10) Specification and verification (program logics, model checking, etc.) (68Q60)

Review text

Summary: Model checking has been extensively used to verify various systems. However, this usually has been done by experts who have a good understanding of model checking and who are familiar with the syntax of both modelling and property specification languages. Unfortunately, this is not an easy task for nonexperts to learn description languages for modelling and formal logics/languages for property specification. In particular, property specification is very daunting and error-prone for nonexperts. In this paper, we present a methodology to facilitate probabilistic model checking for nonexperts. The methodology helps nonexpert users model their systems and express their requirements without any knowledge of the modelling and property specification languages.

Recommendations

• Model checking probabilistic systems
• Model checking of probabilistic and nondeterministic systems
• Abstraction of Probabilistic Systems
• Stochastic model checking
• Verification, Model Checking, and Abstract Interpretation

Cites work

• A Hybrid Approach to Modeling Biological Systems
• A logic for reasoning about time and reliability
• An integrated approach to P systems formal verification
• Automatic verification of real-time systems with discrete probability distributions.
• Combined model checking for temporal, probabilistic, and real-time logics
• Computer Aided Verification
• Computer Aided Verification
• scientific article; zbMATH DE number 2102731 (Why is no real title available?)
• Model-checking in dense real-time
• The Daikon system for dynamic detection of likely invariants

Cited in

(4)

• Spiking neural P systems: matrix representation and formal verification
• Preface to the special issue on probabilistic model checking
• Trade-off analysis meets probabilistic model checking
• Constraint-based debugging in probabilistic model checking

Describes a project that uses

Uses Software

• Ymer
• Kronos
• MRMC
• NuSMV
• PRISM
• SPIN
• Daikon
• ArgoUML

This page was built for publication: Towards light-weight probabilistic model checking

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2336743)