Model-oriented formalisms rely on a combination of safety constraints and satisfaction of refinement obligations to demonstrate model correctness. We argue that for a significant class of models a substantial part of the desired model behaviour would not be covered by such correctness conditions, meaning that a formal development potentially ends with a correct model inadequate for its purpose. In this paper we present a method for augmenting Event-B specifications with additional proof obligations expressed in a visual, diagrammatic way. A case study illustrates how the method may be used to strengthen a model by translating use case scenarios from requirement documents into formal statements over a modelled system. © 2011 Springer-Verlag.
CITATION STYLE
Iliasov, A. (2011). Use case scenarios as verification conditions: Event-B/flow approach. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6968 LNCS, pp. 9–23). https://doi.org/10.1007/978-3-642-24124-6_2
Mendeley helps you to discover research relevant for your work.