Abstract
In Event-B a system is developed using refinement. The language is based on a relatively small core; in particular there is only a very small number of substitutions. This results in much simpler proof obligations, that can be handled by automatic tools. However, the downside is that, in case of software development, structural information is not explicitly available but hidden in the chain of refinements. This paper discusses a method to uncover these implicit algorithmic structures and use them in a model checker. Other applications are code generation, model comprehension, and test-case generation.
This research is being carried out as part of the DFG funded research project GEPAVAS.
Chapter PDF
Similar content being viewed by others
References
Abrial, J.-R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press, Cambridge (2010)
Basin, D.A., Olderog, E.-R., Sevinç, P.E.: Specifying and analyzing security automata using csp-oz. In: Bao, F., Miller, S. (eds.) ASIACCS, pp. 70–81. ACM, New York (2007)
Butler, M.: csp2B: A practical approach to combining CSP and B. Formal Aspects of Computing 12, 182–198 (2000)
Butler, M.: Decomposition structures for event-B. In: Leuschel, M., Wehrheim, H. (eds.) IFM 2009. LNCS, vol. 5423, pp. 20–38. Springer, Heidelberg (2009)
Butler, M., Leuschel, M.: Combining CSP and B for specification and property verification. In: Fitzgerald, J.S., Hayes, I.J., Tarlecki, A. (eds.) FM 2005. LNCS, vol. 3582, pp. 221–236. Springer, Heidelberg (2005)
Fischer, C.: Combining object-z and CSP. In: Wolisz, A., Schieferdecker, I., Rennoch, A. (eds.) FBT, GMD-Studien, vol. 315, pp. 119–128. GMD-Forschungszentrum Informationstechnik GmbH (1997)
Hallerstede, S.: Structured Event-B Models and Proofs. In: Frappier, M., Glässer, U., Khurshid, S., Laleau, R., Reeves, S. (eds.) ABZ 2010. LNCS, vol. 5977, pp. 273–286. Springer, Heidelberg (2010)
Iliasov, A.: Flows Plug-In for Rodin, http://wiki.event-b.org/index.php/Flows#Flows_plugin
Leuschel, M., Butler, M.: ProB: A model checker for B. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, pp. 855–874. Springer, Heidelberg (2003)
Leuschel, M., Butler, M.J.: ProB: an automated analysis toolset for the B method. STTT 10(2), 185–203 (2008)
Leuschel, M., Turner, E.: Visualizing larger states spaces in ProB. In: Treharne, H., King, S., Henson, M., Schneider, S. (eds.) ZB 2005. LNCS, vol. 3455, pp. 6–23. Springer, Heidelberg (2005)
Mahony, B.P., Dong, J.S.: Blending object-z and timed csp: An introduction to tcoz. In: ICSE, pp. 95–104 (1998)
Smith, G., Derrick, J.: Specification, refinement and verification of concurrent systems-an integration of object-z and csp. Formal Methods in System Design 18(3), 249–284 (2001)
Treharne, H., Schneider, S.: How to drive a B machine. In: Bowen, J.P., Dunne, S., Galloway, A., King, S. (eds.) B 2000, ZUM 2000, and ZB 2000. LNCS, vol. 1878, pp. 188–208. Springer, Heidelberg (2000)
Wieczorek, S., Kozyura, V., Roth, A., Leuschel, M., Bendisposto, J., Plagge, D., Schieferdecker, I.: Applying Model Checking to Generate Model-Based Integration Tests from Choreography Models. In: Núñez, M., Baker, P., Merayo, M.G. (eds.) TESTCOM/FATES 2009. LNCS, vol. 5826, pp. 179–194. Springer, Heidelberg (2009)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bendisposto, J., Leuschel, M. (2011). Automatic Flow Analysis for Event-B. In: Giannakopoulou, D., Orejas, F. (eds) Fundamental Approaches to Software Engineering. FASE 2011. Lecture Notes in Computer Science, vol 6603. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-19811-3_5
Download citation
DOI: https://doi.org/10.1007/978-3-642-19811-3_5
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-19810-6
Online ISBN: 978-3-642-19811-3
eBook Packages: Computer ScienceComputer Science (R0)