%S LNCS
%A Alexei Iliasov
%T Use case scenarios as verification conditions: Event-B/Flow approach
%X 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.
%N 6968
%P 9-23
%B Software Engineering for Resilient Systems, Proc. of 3rd International Workshop. September 29-30, 2011 Geneva, Switzerland
%E Elena Troubitsyna
%D 2011
%I Springer
%L deploy315

<script src='//archive-bar.soton.ac.uk/archive-bar.js'></script>