The Efficiency Comparison of the PRISM and Storm Probabilistic Model Checkers for Error Propagation Analysis Tasks

Nafisa Islamovna Yusupova; T. Fabarisov; K. Ding; A. Morozov; K. Janschek

Computer Science and Information Technologies, Computer Science and Information Technologies 2018

Nafisa Islamovna Yusupova, T. Fabarisov, K. Ding, A. Morozov, K. Janschek

Last modified: 2018-10-08

Abstract

Dual-graph Error Propagation Model (DEPM) is a stochastic framework developed in our lab that captures system properties relevant to error propagation processes such as control and data flow structures and reliability characteristics of single components.The DEPM helps to estimate the impact of a fault of a particular component on the overall system reliability. The probability of a system failure, Mean Time Between Failures and Mean Time to Repair, and the expected number of failures are the quantitative results of the DEPM-based analysis. In addition, the DEPM provides an access to the powerful techniques from Probabilistic Model Checking (PMC) that allow the evaluation of advanced, highly customizable, time-related reliability properties, e.g., “the probability of a system failure during certain time units after the occurrence of a certain combination of errors in certain system components”.For this reason, the DEPM models are automatically transformed to discrete-time Markov chain (DTMC) models and are analyzed using the state of the art probabilistic model checker PRISM. However, the new promising model checker Storm has been recently released. This paper presents the results of the efficiency comparison of these two model checkers based on the automatically generated set of the DTMC models that are typical for the error propagation analysis tasks. Several computation engines that are supported by both model checkers have been taking into account. The paper also gives the general description of the DEPM workflow with the focus on the PMC interface.

Keywords

Error propagation model; reliability; safety; dependability; model-based systems; model-based analysis; probabilistic model checking; control flow; data flow; optimization

References

1. Maria Svorenova and Marta Kwiatkowska. Quantitative Verification and Strategy Synthesis for Stochastic Games. European Journal of Control, Elsevier, 2016.

2. A. Morozov and K. Janschek. Dual graph error propagation model for mechatronic system analysis. In 18th IFAC World Congress, Milano, Italy, pages 9893–9898, 2011.

3. A. Morozov, R. Tuk, and K. Janschek. ErrorPro: Software Tool for Stochastic Error Propagation Analysis. In 1st International Workshop on Resiliency in Embedded Electronic Systems, Amsterdam, The Netherlands, pages 59–60, 2015.

4. Fabarisov, T., Yussupova, N., Ding, K., Morozov, A., Janschek, K.: Analytical Toolset for Model-based Stochastic Error Propagation Analysis: Extension and Optimization Towards Industrial Requirements. Proceedings of the 19th international workshop on computer science and information technologies, Germany, Baden-Baden, 2017.

5. A. Morozov and K. Janschek. Probabilistic error propagation model for mechatronic systems. Mechatronics, 24(8):1189 – 1202, 2014.

6. IMC Networks: MTBF, MTTR, MTTF & FIT Explanation of Terms, Aarschot, Belgium, 2011.

7. Marta Kwiatkowska, Gethin Norman, Dave Parker Dave Parker. Probabilistic Model Checking Probabilistic Model Checking, University of Oxford.

8. Vojtěch Forejt, Marta Kwiatkowska, Gethin Norman and David Parker. Automated Verification Techniques for Probabilistic Systems. In M. Bernardo and V. Issarny (editors), Formal Methods for Eternal Networked Software Systems (SFM'11), volume 6659 of LNCS, pages 53-113, Springer. June 2011.

9. Marta Kwiatkowska, Gethin Norman and David Parker. PRISM 4.0: Verification of Probabilistic Real-time Systems. In Proc. 23rd International Conference on Computer Aided Verification (CAV’11), volume 6806 of LNCS, pages 585-591, Springer, 2011.

10. Marta Kwiatkowska, Gethin Norman and David Parker. Probabilistic Verification of Herman’s Self-Stabilisation Algorithm. Formal Aspects of Computing, 24(4), pages 661-670, Springer. July 2012.

11. Christian Dehnert, Sebastian Junges, Joost-Pieter Katoen, Matthias Volk. A Storm is Coming: A Modern Probabilistic Model Checker. Proc. of CAV, Volume 10427 of LNCS, pages 592–600, Springer, 2017.

12. Yuxin Deng, Matthew Hennessy, On the semantics of Markov automata, Information and Computation, Volume 222, 2013, Pages 139-168, ISSN 0890-5401.

13. Tim Quatmann, Christian Dehnert, Nils Jansen, Sebastian Junges, Joost-Pieter Katoen. Parameter Synthesis for Markov Models: Faster Than Ever. Proc. of ATVA, Volume 9938 of LNCS, pages 50–67, Springer, 2016.

14. Christian Dehnert, Sebastian Junges, Joost-Pieter Katoen, Matthias Volk. The Probabilistic Model Checker Storm (Extended Abstract). CoRR abs/1610.08713, 2016.

15. Gethin Norman and David Parker. Quantitative Verification: Formal Guarantees for Timeliness, Reliability and Performance. A report by the London Mathematical Society and the Smith Institute. Edited by Robert Leese and Tom Melham. 2014.

16. Marta Kwiatkowska, Gethin Norman and David Parker. Advances and Challenges of Probabilistic Model Checking. In Proc. 48th Annual Allerton Conference on Communication, Control and Computing, pages 1691-1698, IEEE Press. Invited paper. October 2010.

Full Text: PDF