title: Use case scenarios as verification conditions: Event-B/Flow approach
creator: Iliasov, Alexei
subject: Event-B
subject: Methodology
subject: Tool developments
subject: Model construction
subject: Rodin plug-ins
description: 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.
publisher: Springer
contributor: Troubitsyna, Elena
date: 2011
type: Book Section
type: PeerReviewed
format: application/pdf
identifier: http://deploy-eprints.ecs.soton.ac.uk/315/1/serene2011_submission_14-final.pdf
identifier:   Iliasov, Alexei  (2011) Use case scenarios as verification conditions: Event-B/Flow approach.   In:  Software Engineering for Resilient Systems, Proc. of 3rd International Workshop. September 29-30, 2011 Geneva, Switzerland.   LNCS  (6968).  Springer, pp. 9-23.  ISBN 978-3-642-24123-9     
relation: http://deploy-eprints.ecs.soton.ac.uk/315/