Abstract
When modeling a system using the formal method Event-B, One of the most common problems that may occur during a system processing is infinite cycles. Infinite cycles mean that only certain events are allowed to be executed. In this paper, we present a method to verify the absence of unexecuted events in future system basing on graph theory. This type of verification is not treated by Event-B this mean that even if your system is verified by proof obligations your system is not ensured to occur correctly. In a simple system, it may be very easy to verify that all the events will be executed but in complex system with so many events, it will be impossible. Our method is a verification method based on strongly connected digraph (directed graph), this method verifies the execution of all events in a system and this is why we will call a system verified by our method a strongly connected system.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Butler, M., Abrial, J.R, Banach, R.: Modelling and refining hybrid systems in Event-B and Rodin, chap. 3, pp. 29–42 (2016)
Abrial, J.-R.: Modeling in Event-B: System and Software Design. Cambridge University Press, Cambridge (2008). 586 p.
Hoang, T.S., Kuruma, H., Basin, D., Abrial, J.-R.: Developing topology discovery in Event-B (2009). 19 p.
Ruohonen, K.: Graph Theory. Translation by Janne Tamminen, Kung-Chung Lee and Robert Piché (2013). 110 p.
Peterson, J.L.: Petri Nets. Department of Computer Sciences, The University of Texas, Austin, Texas 78712 (1977)
Geeraerts, G.: An Introduction to Petri nets and how to analyse them…, Groupe de Vérification Département d’Informatique Université Libre de Bruxelles, 165 p.
Wilson, R.J.: Introduction to Graph Theory, 4th edn. Longman Group Ltd. (1998), 171 p. ISBN 0-582-24993-7
Diestel, R., Kuhn, D.: On infinite cycles II. Combinatorica 24(1), 91–116 (2004)
Bruhn, H., Stein, M.: On end degrees and infinite cycles in locally finite graphs. Combinatorica 27(3), 269–291 (2007)
Sharir, M.: A strong connectivity algorithm and its applications to data flow analysis. Comput. Math Appl. 7, 67–72 (1981)
Cormen, T.H., Leiserson, C.E., Rivest, R.L., Stein, C.: Introduction to Algorithms, 3rd edn. The MIT Press, Cambridge (2009). ISBN 0-262-03384-4
Aho, A.V., Hopcroft, J.E., Ullman, J.D.: Data Structures and Algorithms. Addison-Wesley, Boston (1983)
Jarrar, A., Balouki, Y.: Formal modeling of a complex adaptive air traffic control system. Complex Adapt. Syst. Model. 6(1), 6 (2018)
Vistbakka, I., Troubitsyna, E.: Towards integrated modelling of dynamic access control with UML and Event-B. arXiv preprint arXiv:1805.05521 (2018)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2019 Springer Nature Switzerland AG
About this paper
Cite this paper
Jarrar, A., Gadi, T., Balouki, Y. (2019). New Approach for Solving Infinite Cycles Problem During Modeling. In: Khoukhi, F., Bahaj, M., Ezziyyani, M. (eds) Smart Data and Computational Intelligence. AIT2S 2018. Lecture Notes in Networks and Systems, vol 66. Springer, Cham. https://doi.org/10.1007/978-3-030-11914-0_26
Download citation
DOI: https://doi.org/10.1007/978-3-030-11914-0_26
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-11913-3
Online ISBN: 978-3-030-11914-0
eBook Packages: Intelligent Technologies and RoboticsIntelligent Technologies and Robotics (R0)