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. © 2011 Springer-Verlag.
CITATION STYLE
Bendisposto, J., & Leuschel, M. (2011). Automatic flow analysis for event-B. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6603 LNCS, pp. 50–64). https://doi.org/10.1007/978-3-642-19811-3_5
Mendeley helps you to discover research relevant for your work.