Open Access Open Access  Restricted Access Subscription or Fee Access

Verification of Infinite Loops’ Absence in Event-B Models


(*) Corresponding author


Authors' affiliations


DOI: https://doi.org/10.15866/iremos.v12i3.16303

Abstract


The development of complex systems remains one of the most critical problems in computer science. However, most of these systems are safety-critical and require a lot of care during modelling and designing. Therefore, researchers have proposed sophisticated tools and techniques in order to minimize the risk of failure in these systems. One of the most powerful tools in the domain is the Event-B formal method. It provides a set of proofs that ensure a strong assurance of bugs’ absence. Anyway, it is not perfect and it does not treat all the possible issues such as infinite cycles, which is a case where only certain events will loop forever. The goal of this paper is to propose a method based on graph theory in order to verify the absence of these cycles and to prevent having unexecuted functionalities (events) in the system. In a system with few elements, it may be easy to verify manually the absence of infinite cycles but it is not the case for complex systems. The proposed method allows the verification of infinite cycles’ absence using the strongly connected directed graph (digraph) concept. This means that the occurrence of all events in a system is guaranteed, therefore, a system verified by the proposed method can be called strongly connected system.
Copyright © 2019 Praise Worthy Prize - All rights reserved.

Keywords


Formal Methods; Event-B; Infinite Cycle; Graph Theory; Strongly Connected Digraph

Full Text:

PDF


References


Dupont, G., Aït-Ameur, Y., Pantel, M., & Singh, N. K. (2018, June). Proof-Based approach to hybrid systems development: dynamic logic and Event-B. In International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z (pp. 155-170). Springer, Cham.
https://doi.org/10.1007/978-3-319-91271-4_11

Jean-Raymond Abrial, Modeling in Event-B: System and Software Design. Cambridge University Press, 586 p, 2008.

Abrial, J. R. (2018, June). On B and Event-B: Principles, Success and Challenges. In International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z (pp. 31-35). Springer, Cham.
https://doi.org/10.1007/978-3-319-91271-4_3

Watson, C. G., DeMaster, D., and Ewing-Cobbs, L. (2019). Graph theory analysis of DTI tractography in children with traumatic injury. NeuroImage: Clinical, 21, 101673.
https://doi.org/10.1016/j.nicl.2019.101673

Snene, W., Mechri, W., Ben Othman, K., Interval Valued Generalized Stochastic Petri Nets for Imprecise Modeling in Unavailability Assessment, (2017) International Review of Electrical Engineering (IREE), 12 (5), pp. 399-408.
https://doi.org/10.15866/iree.v12i5.11920

Bennoui, H., Chaoui, A., Backward Reachability Analysis Based on BPNs to Model-Based Diagnosis with Relationships among Symptoms, (2018) International Journal on Computer and Communications Networks, Computational Intelligence and Data Analytics, 2 (2), pp. 50-55.

Moreno-Chuquen, R., Obando-Ceron, J., Network Topological Notions for Power Systems Security Assessment, (2018) International Review of Electrical Engineering (IREE), 13 (3), pp. 237-245.
https://doi.org/10.15866/iree.v13i3.14210

Hammond, A., & Hegde, M. (2018). Critical point for infinite cycles in a random loop model on trees. arXiv preprint arXiv:1805.11772.

Ryan, C. T., Smith, R. L., & Epelman, M. A. (2018). A simplex method for uncapacitated pure-supply infinite network flow problems. SIAM Journal on Optimization, 28(3), 2022-2048.
https://doi.org/10.1137/17m1137553

Georgiadis, L., Italiano, G. F., & Parotsidis, N. (2018, April). Incremental strong connectivity and 2-connectivity in directed graphs. In Latin American Symposium on Theoretical Informatics (pp. 529-543). Springer, Cham.
https://doi.org/10.1007/978-3-319-77404-6_39

Zeng, M., Yang, X., Wang, M., & Xu, B. (2018). Application of Angle Related Cost Function Optimization for Dynamic Path Planning Algorithm. Algorithms, 11(8), 127.
https://doi.org/10.3390/a11080127

Sun, X., Ye, X., Kang, K., Xu, L., Wang, W., & Lv, L. (2019, April). BSP-Based Strongly Connected Component Algorithm in Joint Cloud Computing. In 2019 IEEE International Conference on Service-Oriented System Engineering (SOSE) (pp. 287-2875). IEEE.
https://doi.org/10.1109/sose.2019.00049

Jarrar, A., & Balouki, Y. (2018). Formal modeling of a complex adaptive air traffic control system. Complex Adaptive Systems Modeling, 6(1), 6.
https://doi.org/10.1186/s40294-018-0056-4

Vistbakka, I., & Troubitsyna, E. Towards Integrated Modelling of Dynamic Access Control with UML and Event-B. arXiv preprint arXiv:1805.05521 (2018).

Zhang, Y., Liao, X., Shi, X., Jin, H., & He, B. (2018). Efficient disk-based directed graph processing: A strongly connected component approach. IEEE Transactions on Parallel and Distributed Systems, 29(4), 830-842.
https://doi.org/10.1109/tpds.2017.2776115

Blelloch, G. E., Gu, Y., Sun, Y., & Shun, J. (2018). Parallel write-efficient algorithms and data structures for computational geometry. arXiv preprint arXiv:1805.05592.
https://doi.org/10.1145/3210377.3210380

Dalvandi, M., Butler, M., Rezazadeh, A., & Fathabadi, A. S. (2018, June). Verifiable Code Generation from Scheduled Event-B Models. In International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z (pp. 234-248). Springer, Cham.
https://doi.org/10.1007/978-3-319-91271-4_16

Carbin, M., Misailovic, S., Kling, M., & Rinard, M. C. (2011, July). Detecting and escaping infinite loops with jolt. In European Conference on Object-Oriented Programming (pp. 609-633). Springer, Berlin, Heidelberg.
https://doi.org/10.1007/978-3-642-22655-7_28

Burnim, J., Jalbert, N., Stergiou, C., & Sen, K. (2009, November). Looper: Lightweight detection of infinite loops at runtime. In Proceedings of the 2009 IEEE/ACM International Conference on Automated Software Engineering (pp. 161-169). IEEE Computer Society.
https://doi.org/10.1109/ase.2009.87

Inggs, C. P., & Barringer, H. (2002). Effective state exploration for model checking on a shared memory architecture. Electronic Notes in Theoretical Computer Science, 68(4), 605-620.
https://doi.org/10.1016/s1571-0661(05)80395-0

Ait Wakrime, A., Ayed, R. B., Collart-Dutilleul, S., Ledru, Y., & Idani, A. (2018, October). Formalizing railway signaling system ERTMS/ETCS using UML/Event-B. In International Conference on Model and Data Engineering (pp. 321-330). Springer, Cham.
https://doi.org/10.1007/978-3-030-00856-7_21

Jarrar, A., Gadi, T., & Balouki, Y. (2018, October). New Approach for Solving Infinite Cycles Problem During Modeling. In International Conference on Advanced Information Technology, Services and Systems (pp. 241-248). Springer, Cham.
https://doi.org/10.1007/978-3-030-11914-0_26

Ait Wakrime, A., Gibson, J. P., & Raffy, J. L. (2018, June). Formalising the Requirements of an E-Voting Software Product Line Using Event-B. In 2018 IEEE 27th International Conference on Enabling Technologies: Infrastructure for Collaborative Enterprises (WETICE), pp. 78-84, IEEE.
https://doi.org/10.1109/wetice.2018.00022


Refbacks

  • There are currently no refbacks.



Please send any question about this web site to info@praiseworthyprize.com
Copyright © 2005-2024 Praise Worthy Prize