A Formal Approach for Maintainability and Availability Assessment Using Probabilistic Model Checking

  • Abdelhakim BaouyaEmail author
  • Djamal Bennouar
  • Otmane Ait Mohamed
  • Samir Ouchani
Conference paper
Part of the Lecture Notes in Networks and Systems book series (LNNS, volume 1)


Availability is one of the crucial characteristics that measures the system quality and influences the users and system designers. The aim of this work is to provide an approach to improve the system availability by taking into account different system situations at design step using SysML state machine diagram. We construct a formal model of state machine in the probabilistic calculus which supports modeling of concurrency and uncertainty. In this paper, we consider a single industrial control equipment and a multiprocessing computing platform where its behavior is modeled by SysML state machine diagram and we use logical specification of maintainability and availability properties. The probabilistic model checker PRISM has been used to perform quantitative analyses of these properties.


SysML state machine diagram Reliability Availability Maintainability 



This research was performed as part of the LIMPAF/CNEPRU/C00L07UN100120110008 project supported by the Algerian Ministry of Higher Education and Scientific Research and the LIMPAF Lab at the University of Bouira, Algeria.


  1. 1.
    Baier, C., Katoen, J.P.: Principles of Model Checking (Representation and Mind Series). The MIT Press (2008)Google Scholar
  2. 2.
    Baouya, A., Bennouar, D., Ait Mohamed, O., Ouchani, S.: On the probabilistic verification of time constrained sysml state machines. In: Fujita, H., Guizzi, G. (eds.) Intelligent Software Methodologies, Tools and Techniques, Communications in Computer and Information Science, vol. 532, pp. 425–441. Springer International Publishing (2015)Google Scholar
  3. 3.
    Behrmann, G., David, A., Larsen, K.G.: A tutorial on uppaal. In: Formal Methods for the Design of Real-Time Systems, pp. 200–236 (2004)Google Scholar
  4. 4.
    Birolini, A.: Reliability engineering: theory and practice. Basic Concepts, Quality and Reliability (RAMS) Assurance of Complex Equipment and Systems, pp. 1–24. Springer, Berlin (2014)Google Scholar
  5. 5.
    Calinescu, R., Ghezzi, C., Johnson, K., Pezze, M., Rafiq, Y., Tamburrelli, G.: Formal verification with confidence intervals to establish quality of service properties of software systems. IEEE Trans. Reliab. 99, 1–19 (2015)Google Scholar
  6. 6.
    Dhouibi, M., Saintis, L., Barreau, M., Perquis, J.M.: Safety driven optimization approach for automotive systems. In: Reliability and Maintainability Symposium (RAMS), 2015 Annual, pp. 1–7 (2015)Google Scholar
  7. 7.
    Franco, J., Barbosa, R., Zenha-Rela, M.: Reliability analysis of software architecture evolution. In: 2013 Sixth Latin-American Symposium on Dependable Computing (LADC), pp. 11–20 (2013)Google Scholar
  8. 8.
    Ghadhab, M., Kuntz, M., D.K., Fetzer, C.: Formal techniques for safety-critical systems. In: Fourth International Workshop, FTSCS 2015, Paris, France, November 6 and 7, 2015. Springer International Publishing (2016)Google Scholar
  9. 9.
    Hahn, E.M., Han, T., Zhang, L.: Synthesis for PCTL in parametric Markov decision processes. In: Proceedings of 3rd NASA Formal Methods Symposium (NFM’11). LNCS, vol. 6617. Springer (2011)Google Scholar
  10. 10.
    Houssin, R., Coulibaly, A.: Safety-based availability assessment at design stage. Comput. Ind. Eng. 70, 107–115 (2014)CrossRefGoogle Scholar
  11. 11.
    Hoque, K., Ait Mohamed, O., Savaria, Y., Thibeault, C.: Early analysis of soft error effects for aerospace applications using probabilistic model checking. In: Artho, C., Ölveczky, P.C. (eds.) Formal Techniques for Safety-Critical Systems, Communications in Computer and Information Science, vol. 419, pp. 54–70. Springer International Publishing (2014)Google Scholar
  12. 12.
    Huang, X., Sun, Q., Li, J., Pan, M., Zhang, T.: An mde-based approach to the verification of sysml state machine diagram. In: Proceedings of the Fourth Asia-Pacific Symposium on Internetware. Internetware’12, pp. 9:1–9:7. ACM, New York (2012)Google Scholar
  13. 13.
    Kwiatkowska, M., Norman, G., Parker, D.: Stochastic model checking. In: Bernardo, M., Hillston, J. (eds.) Formal Methods for the Design of Computer, Communication and Software Systems: Performance Evaluation (SFM’07). LNCS (Tutorial Volume), vol. 4486, pp. 220–270. Springer (2007)Google Scholar
  14. 14.
    Kwiatkowska, M.Z., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Computer Aided Verification–23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings, pp. 585–591 (2011)Google Scholar
  15. 15.
    Kwiatkowska, M., Norman, G., Parker, D.: Prism: Probabilistic model checking for performance and reliability analysis. SIGMETRICS Perform. Eval. Rev. 36(4), 40–45 (2009)CrossRefGoogle Scholar
  16. 16.
    Lazzaroni, M., Cristaldi, L., Peretto, L., Rinaldi, P., Catelani, M.: Reliability engineering: basic concepts and applications in ICT. Repairable Systems and Availability, pp. 85–92. Springer, Berlin (2011)Google Scholar
  17. 17.
    Liu, Y., Shen, G., Huang, Z., Yang, Z.: Quantitative risk analysis of safety–critical embedded systems. Softw. Qual. J. 1–25 (2016)Google Scholar
  18. 18.
    Lu, Y., Peng, Z., Miller, A.A., Zhao, T., Johnson, C.W.: How reliable is satellite navigation for aviation? Checking availability properties with probabilistic verification. Reliab. Eng. Syst. Saf. 144, 95–116 (2015)CrossRefGoogle Scholar
  19. 19.
    Mallet, F., de Simone, R.: MARTE: a profile for RT/E systems modeling, analysis and simulation. In: Proceedings of the 1st International Conference on Simulation Tools and Techniques for Communications, Networks and Systems and Workshops, SimuTools 2008, Marseille, France, March 3–7, 2008, p. 43 (2008)Google Scholar
  20. 20.
    Morant, A., Gustafson, A., Söderholm, P.: Safety and availability evaluation of railway signalling systems. In: Kumar, U., Ahmadi, A., Verma, A.K., Varde, P. (eds.) Current Trends in Reliability, Availability, Maintainability and Safety, Lecture Notes in Mechanical Engineering, pp. 303–316. Springer International Publishing (2016)Google Scholar
  21. 21.
    Norman, G., Parker, D.: Quantitative verification: Formal guarantees for timeliness, reliability and performance. Technical Report. The London Mathematical Society and the Smith Institute (2014)Google Scholar
  22. 22.
    O.M. Group (ed.): OMG Systems Modeling Language (Object Management Group SysML) (2012)Google Scholar
  23. 23.
    Ouchani, S., Aït Mohamed, O., Debbabi, M.: A property-based abstraction framework for sysml activity diagrams. Knowl. Based Syst. 56, 328–343 (2014)Google Scholar
  24. 24.
    Peng, Z., Lu, Y., Miller, A., Johnson, C., Zhao, T.: A probabilistic model checking approach to analysing reliability, availability, and maintainability of a single satellite system. In: Modelling Symposium (EMS), 2013 European, pp. 611–616 (2013)Google Scholar
  25. 25.
    Qiu, S., Sallak, M., Schön, W., Cherfi-Boulanger, Z.: Availability assessment of railway signalling systems with uncertainty analysis using statecharts. Simul. Model. Pract. Theory 47, 1–18 (2014)CrossRefGoogle Scholar
  26. 26.
    Reliasoft: Lambda Predict.
  27. 27.
    Sivanandam, S.N., Deepa, S.N.: Introduction to Genetic Algorithms, 1st edn. Springer Publishing Company (2010) (Incorporated)Google Scholar
  28. 28.
    Song, L., Zhang, L., Godskesen, J.: Bisimulations and logical characterizations on continuous-time markov decision processes. In: McMillan, K., Rival, X. (eds.) Verification, Model Checking, and Abstract Interpretation. Lecture Notes in Computer Science, vol. 8318, pp. 98–117. Springer, Berlin (2014)Google Scholar
  29. 29.
    Tian, Y., Wan, L., hung Chen, C., Yang, Y.: Safety assessment method of performance-based navigation airspace planning. J. Traffic Transp. Eng. (English Edition) 2(5), 338–345 (2015)Google Scholar

Copyright information

© Springer International Publishing Switzerland 2016

Authors and Affiliations

  • Abdelhakim Baouya
    • 1
    Email author
  • Djamal Bennouar
    • 2
  • Otmane Ait Mohamed
    • 3
  • Samir Ouchani
    • 4
  1. 1.LIMPAF Lab, CS DepartmentUniversity of BlidaBlidaAlgeria
  2. 2.LIMPAF Lab, CS DepartmentUniversity of BouiraBouiraAlgeria
  3. 3.ECE DepartmentConcordia UniversityMontrealCanada
  4. 4.SnT CenterUniversity of LuxembourgLuxembourg CityLuxembourg

Personalised recommendations