Modeling and analysis of probabilistic real-time systems through integrating event-b and probabilistic model checking

• Autorzy: Debbi Hichem

Identyfikatory

DOI

10.7494/csci.2022.23.4.4588

• Języki publikacji: EN

Abstrakty

EN

Event-B is a formal method that is used in the development of safety-critical systems; however, these systems may introduce uncertainty and also need to meet real-time requirements, which make the modeling and analysis of such systems a challenging task. While some works exist that try to extend Event-B with probability and over time, they fail to address both in a single framework. Besides, these works mainly addressed extending the language itself, not integrating extended Event-B with verification. In this paper, we aim to represent both probability and time in the Event-B language, and we will show how such a representation can be automatically translated into the probabilistic timed automata (PTA) that are described in the language of the PRISM probabilistic model checker. This transformation approach would allow us to analyze the probabilistic and time-bounded probabilistic reachability properties of probabilistic real-time systems through probabilistic timed CTL (PTCTL) logic.

Słowa kluczowe

EN

event-B; probabilistic event-B; real-time probabilistic model checking; PTA; PRISM

• Wydawca: Wydawnictwa AGH
• Czasopismo: Computer Science
• Rocznik: 2022
• Tom: T. 23 (4)
• Strony: 545--570
• Opis fizyczny: Bibliogr. 36 poz., rys., tab.

Twórcy

autor

Debbi Hichem

• University of Msila, Department of Computer Science, Msila, Algeria

Bibliografia

• [1] Abrial J.R.: Modeling in Event-B: System and Software Engineering, Cambridge University Press, 2010.
• [2] Abrial J.R., Cansell D., Mery D.: A Mechanically Proved and Incremental Development of IEEE 1394 Tree Identify Protocol, Formal Aspects of Computing, vol. 14, pp. 215–227, 2003.
• [3] Alur R.: Timed Automata. In: N. Halbwachs, D. Peled (eds.), Computer Aided Verification, pp. 8–22, 1999.
• [4] Aouadhi M., Delahaye B., Lanoix A.: Introducing probabilistic reasoning within Event-B, Software & Systems Modeling, vol. 18, pp. 1953–1984, 2019.
• [5] Bengtsson J., Larsen K., Larsson F., Pettersson P., Yi W.: UPPAAL – a tool suite for automatic verification of real-time systems. In: R. Alur, T.A. Henzinger, E.D. Sontag (eds.), Hybrid Systems III. Verification and Control, Lecture Notes in Computer Science, vol. 1066, pp. 232–243, Springer, Berlin–Heidelberg, 1996. doi: 10.1007/BFb0020949.
• [6] Butler M.: Decomposition Structures for Event-B. In: Integrated Formal Methods, pp. 20–38, Springer, Berlin–Heidelberg, 2009.
• [7] Cansell D., Mery D., Rehm J.: Time Constraint Patterns for Event B Development. In: B 2007: Formal Specification and Development in B, pp. 140–154, Springer, Berlin–Heidelberg, 2006. doi: 10.1007/11955757 13.
• [8] Cimatti A., Clarke E., Giunchiglia F., Roveri M.: NUSMV: a new symbolic model checker, International Journal on Software Tools for Technology Transfer, vol. 2, pp. 410–425, 2000.
• [9] Dalvandi M., Butler M., Rezazadeh A.: From Event-B Models to Dafny Code Contracts. In: Fundamentals of Software Engineering. FSEN 2015, p. 308–315, Springer-Verlag.
• [10] Daws C., Kwiatkowska M., Norman G.: Automatic verification of the IEEE 1394 root contention protocol with KRONOS and PRISM, International Journal on Software Tools for Technology Transfer volume, vol. 5, pp. 221–236, 2004. doi: 10.1007/s10009-003-0118-5.
• [11] Dijkstra E.W.: A Discipline of Programming, Prentice Hall International, Englewood Cliffs, N.J., 1976.
• [12] Duflot M., Fribourg L., Herault T., Lassaigne R., Magniette F., Messika S., Peyronnet S., Picaronny C.: Probabilistic Model Checking of the CSMA/CD protocol using PRISM and APMC, Electronic Notes in Theoretical Computer Science, vol. 128(6), pp. 195–214, 2004. doi: 10.1016/j.entcs.2005.04.012.
• [13] Hadad A.S.A., Ma C., Ahmed A.A.O.: Formal Verification of AADL Models by Event-B, IEEE Access, vol. 8, pp. 72814–72834, 2020. doi: 10.1109/ ACCESS.2020.2987972.
• [14] Hallerstede S., Hoang T.S.: Qualitative Probabilistic Modelling in Event-B. In: J. Davies, J. Gibbons (eds.), Integrated Formal Methods. IFM 2007, Lecture Notes in Computer Science, vol. 4591, pp. 293–312, Springer, Berlin–Heidelberg, 2007. doi: 10.1007/978-3-540-73210-5 16.
• [15] Hansson H., Jonsson B.: A logic for reasoning about time and reliability, Formal Aspects of Computing, vol. 6(5), pp. 512–535, 1994.
• [16] Henzinger T.A., Nicollin X., Sifakis J., Yovine S.: Symbolic Model Checking for Real-Time Systems, Information and Computation, vol. 111(2), pp. 193–244, 1994. doi: 10.1006/inco.1994.1045.
• [17] Hinton A., Kwiatkowska M., Norman G., Parker D.: PRISM: A tool for automatic verification of probabilistic systems. In: H. Hermanns, J. Palsberg (eds.), Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2006, Lecture Notes in Computer Science, vol. 3920, pp. 441–444, Springer, Berlin– Heidelberg, 2006. doi: 10.1007/11691372 29.
• [18] Hoang T.S.: The Development of a Probabilistic B-Method and a Supporting Toolkit, Ph.D. thesis, School of Computer Science and Engineering, UNSW, 2005.
• [19] Holzmann G.: The SPIN Model Checker: Primer and Reference Manual, Addison Wesley, 2004.
• [20] Iliasov A., Romanovsky A., Laibinis L., Troubitsyna E., Latvala T.: Augmenting Event-B modelling with real-time verification. In: 2012 First International Workshop on Formal Methods in Software Engineering: Rigorous and Agile Approaches (FormSERA), p. 51–57, 2012. doi: 10.1109/FormSERA.2012.6229789.
• [21] Katoen J.P., Khattri M., Zapreev I.S.: A Markov reward model checker. In: Second International Conference on the Quantitative Evaluation of Systems (QEST’05), pp. 243–244, 2005. doi: 10.1109/QEST.2005.2.
• [22] Kozen D.: A probabilistic PDL, Journal of Computer and System Sciences, vol. 30(2), pp. 162–178, 1985.
• [23] Kwiatkowska M., Norman G., Segala R., Sproston J.: Automatic verification of real-time systems with discrete probability distributions, Theoretical Computer Science, vol. 286(1), pp. 101–150, 2002.
• [24] Kwiatkowska M., Norman G., Sproston J.: Probabilistic Model Checking of Deadline Properties in the IEEE 1394 FireWire Root Contention Protocol, Formal Aspects of Computing, vol. 14(3), p. 295–318, 2003.
• [25] Kwiatkowska M., Norman G., Sproston J., Wang F.: Symbolic model checking for probabilistic timed automata, Information and Computation, vol. 205(7), pp. 1027–1077, 2007.
• [26] Mery D., Rosemary M.: Transforming EVENT B Models into Verified C# Implementations. In: A. Lisitsa, A. Nemytykh (eds.), VPT 2013 – First International Workshop on Verification and Program Transformation, EPIC, vol. 16, pp. 57–73, 2013. https://hal.inria.fr/hal-00862050.
• [27] Michael L., Michael B.: ProB: A Model Checker for B. In: FME 2003: Formal Methods, pp. 855–874, Springer, Berlin–Heidelberg, 2003.
• [28] Morgan C., Hoang T.S., Abrial J.R.: The Challenge of Probabilistic Event B. In: ZB 2005: Formal Specification and Development in Z and B, Lecture Notes in Computer Science, vol. 3455, pp. 162–171, Springer, Berlin–Heidelberg, 2005. doi: 10.1007/11415787 10.
• [29] Ndukwu U., McIver A.K.: YAGA: Automated Analysis of Quantitative Safety Specifications in Probabilistic B. In: A. Bouajjani, W.N. Chin (eds.), Automated Technology for Verification and Analysis, Lecture Notes in Computer Science, vol. 6252, pp. 378–386, Springer, Berlin–Heidelberg, 2010. doi: 10.1007/978-3- 642-15643-4 31.
• [30] nuXmv: https://nuxmv.fbk.eu/.
• [31] PRISM benchmark suite – Models. http: / /www.prismmo d elchecker.org / benchmarks/models.php.
• [32] Sena L., Xiangyu L., Zuxi C.: Combining Theorem Proving and Model Checking in the Safety-Critical Software Development through Translating Event-B to SMV. In: MATEC Web Conf, vol. 128, 2017. doi: 10.1051/matecconf/ 201712804004.
• [33] Tarasyuk A., Troubitsyna E., Laibinis L.: Towards Probabilistic Modelling in Event-B. In: Integrated Formal Methods, Lecture Notes in Computer Science, vol. 6396, pp. 275–289, Springer, Berlin–Heidelberg, 2010. doi: 10.1007/978-3- 642-16265-7 20.
• [34] Tarasyuk A., Troubitsyna E., Laibinis L.: Formal Modelling and Verification of Service-Oriented Systems in Probabilistic Event-B. In: Integrated Formal Methods, Lecture Notes in Computer Science, vol. 7321, pp. 237–252, Springer, Berlin– Heidelberg, 2012. doi: 10.1007/978-3-642-30729-4 17.
• [35] Tarasyuk A., Pereverzeva I., Troubitsyna E., Laibinis L.: Formal Development and Quantitative Assessment of a Resilient Multi-robotic System. In: A. Gorbenko, A. Romanovsky, V. Kharchenko (eds.), Software Engineering for Resilient Systems, Lecture Notes in Computer Science, vol. 8166, pp. 109–124, Springer, Berlin–Heidelberg, 2013. doi: 10.1007/978-3-642-40894-6 9.
• [36] Thomas M., Shin N.: Rodin Plugin to Link Event-B and SPIN. Technical Report, IEICE Digital Library, 2009.

Uwagi

PL

Opracowanie rekordu ze środków MEiN, umowa nr SONP/SP/546092/2022 w ramach programu "Społeczna odpowiedzialność nauki" - moduł: Popularyzacja nauki i promocja sportu (2022-2023).