Abstract
Event-B is a formal method for reliable systems specification and verification, which uses model refinement and decomposition as techniques to scale the design of complex systems. In previous work, we proposed an iterative approach for test generation and state model inference based on a variant of Angluin’s learning algorithm, which integrates well with the notion of Event-B refinement. In this paper, we extend the method to work also with the mechanisms of Event-B decomposition. Two types of decomposition, i.e. shared-events and shared-variables, are considered and the generation of a global test suite from the local ones is proposed at the end. The implementation of the method is evaluated on publicly available Event-B decomposed models.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Abrial, J.-R.: Modeling in Event-B – System and Software Engineering. Cambridge University Press (2010)
Silva, R., Pascal, C., Son Hoang, T., Butler, M.: Decomposition tool for Event-B. Softw., Pract. Exper. 41(2), 199–208 (2011), Plug-in webpage: http://wiki.event-b.org/index.php/Event_Model_Decomposition
Son Hoang, T., Iliasov, A., Silva, R., Wei, W.: A survey on Event-B decomposition. ECEASST 46, 1–15 (2011)
Butler, M.: Decomposition Structures for Event-B. In: Leuschel, M., Wehrheim, H. (eds.) IFM 2009. LNCS, vol. 5423, pp. 20–38. Springer, Heidelberg (2009)
Silva, R., Butler, M.: Shared Event Composition/Decomposition in Event-B. In: Aichernig, B.K., de Boer, F.S., Bonsangue, M.M. (eds.) FMCO 2010. LNCS, vol. 6957, pp. 122–141. Springer, Heidelberg (2011)
Abrial, J.-R.: Event model decomposition. Technical Report 626, ETH Zurich (May 2009)
Hoang, T.S., Abrial, J.-R.: Event-B Decomposition for Parallel Programs. In: Frappier, M., Glässer, U., Khurshid, S., Laleau, R., Reeves, S. (eds.) ABZ 2010. LNCS, vol. 5977, pp. 319–333. Springer, Heidelberg (2010)
Abrial, J.-R., Butler, M., Hallerstede, S., Hoang, T.S., Mehta, F., Voisin, L.: Rodin: an open toolset for modelling and reasoning in Event-B. STTT 12(6), 447–466 (2010), Tool available online at: http://sourceforge.net/projects/rodin-b-sharp
Lee, D., Yannakakis, M.: Principles and methods of testing finite state machines – A survey. Proc. of the IEEE 84(8), 1090–1123 (1996)
Ipate, F.: Bounded sequence testing from deterministic finite state machines. Theoret. Comput. Sci. 411(16-18), 1770–1784 (2010)
Ipate, F., Dinca, I., Stefanescu, A.: Model learning and test generation using cover automata (submitted, 2012)
Dinca, I., Ipate, F., Stefanescu, A.: Learn and Test for Event-B – A Rodin Plugin. In: Derrick, J., Fitzgerald, J., Gnesi, S., Khurshid, S., Leuschel, M., Reeves, S., Riccobene, E. (eds.) ABZ 2012. LNCS, vol. 7316, pp. 361–364. Springer, Heidelberg (2012), Plug-in webpage: http://wiki.event-b.org/index.php/MBT_plugin
Angluin, D.: Learning regular sets from queries and counterexamples. Inf. Comput. 75(2), 87–106 (1987)
Ipate, F.: Learning finite cover automata from queries. Journal of Computer and System Sciences 78, 221–244 (2012)
Câmpeanu, C., Sântean, N., Yu, S.: Minimal cover-automata for finite languages. Theoret. Comput. Sci. 267(1-2), 3–16 (2001)
Hopcroft, J.E., Motwani, R., Ullman, J.D.: Introduction to Automata Theory, Languages, and Computation, 3rd edn. Addison-Wesley (2006)
Pasareanu, C.S., Giannakopoulou, D., Bobaru, M.G., Cobleigh, J.M., Barringer, H.: Learning to divide and conquer: applying the L * algorithm to automate assume-guarantee reasoning. Formal Methods in System Design 32(3), 175–205 (2008)
Thiagarajan, P.S.: A Trace Consistent Subset of PTL. In: Lee, I., Smolka, S.A. (eds.) CONCUR 1995. LNCS, vol. 962, pp. 438–452. Springer, Heidelberg (1995)
Salehi Fathabadi, A., Rezazadeh, A., Butler, M.: Applying Atomicity and Model Decomposition to a Space Craft System in Event-B. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 328–342. Springer, Heidelberg (2011)
Iliasov, A., Troubitsyna, E., Laibinis, L., Romanovsky, A., Varpaaniemi, K., Ilic, D., Latvala, T.: Supporting Reuse in Event B Development: Modularisation Approach. In: Frappier, M., Glässer, U., Khurshid, S., Laleau, R., Reeves, S. (eds.) ABZ 2010. LNCS, vol. 5977, pp. 174–188. Springer, Heidelberg (2010), http://wiki.event-b.org/index.php/Modularisation_Plug-in
Poppleton, M.: The Composition of Event-B Models. In: Börger, E., Butler, M., Bowen, J.P., Boca, P. (eds.) ABZ 2008. LNCS, vol. 5238, pp. 209–222. Springer, Heidelberg (2008), http://wiki.event-b.org/index.php/Parallel_Composition_using_Event-B
http://tinyurl.com/isola12-with-appendix – extended version of our paper
Jirásková, G., Masopust, T.: State Complexity of Projected Languages. In: Holzer, M. (ed.) DCFS 2011. LNCS, vol. 6808, pp. 198–211. Springer, Heidelberg (2011)
Julliand, J., Stouls, N., Bué, P.-C., Masson, P.-A.: Syntactic Abstraction of B Models to Generate Tests. In: Fraser, G., Gargantini, A. (eds.) TAP 2010. LNCS, vol. 6143, pp. 151–166. Springer, Heidelberg (2010)
Shahbaz, M., Li, K., Groz, R.: Learning and Integration of Parameterized Components Through Testing. In: Petrenko, A., Veanes, M., Tretmans, J., Grieskamp, W. (eds.) TestCom/FATES 2007. LNCS, vol. 4581, pp. 319–334. Springer, Heidelberg (2007)
Berg, T., Grinchtein, O., Jonsson, B., Leucker, M., Raffelt, H., Steffen, B.: On the Correspondence Between Conformance Testing and Regular Inference. In: Cerioli, M. (ed.) FASE 2005. LNCS, vol. 3442, pp. 175–189. Springer, Heidelberg (2005)
Bollig, B., Katoen, J.-P., Kern, C., Leucker, M.: Learning communicating automata from MSCs. IEEE Trans. Software Eng. 36(3), 390–408 (2010)
Bohlin, T., Jonsson, B., Soleimanifard, S.: Inferring Compact Models of Communication Protocol Entities. In: Margaria, T., Steffen, B. (eds.) ISoLA 2010, Part I. LNCS, vol. 6415, pp. 658–672. Springer, Heidelberg (2010)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Dinca, I., Ipate, F., Stefanescu, A. (2012). Model Learning and Test Generation for Event-B Decomposition. In: Margaria, T., Steffen, B. (eds) Leveraging Applications of Formal Methods, Verification and Validation. Technologies for Mastering Change. ISoLA 2012. Lecture Notes in Computer Science, vol 7609. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-34026-0_40
Download citation
DOI: https://doi.org/10.1007/978-3-642-34026-0_40
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-34025-3
Online ISBN: 978-3-642-34026-0
eBook Packages: Computer ScienceComputer Science (R0)