creators_name: Iliasov, Alexei creators_id: "Alexei Iliasov" editors_name: Troubitsyna, Elena editors_id: Elena.Troubitsyna@abo.fi type: book_section datestamp: 2011-07-04 12:44:57 lastmod: 2011-10-29 18:28:41 metadata_visibility: show title: Use case scenarios as verification conditions: Event-B/Flow approach ispublished: pub subjects: Event-Bsemantics subjects: deploy_method subjects: deploy_tooldev subjects: deploy_tooldev_modelc subjects: deploy_tooldev_rodinplugins full_text_status: public abstract: 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. date: 2011 date_type: published series: LNCS number: 6968 publisher: Springer pagerange: 9-23 pages: 15 refereed: TRUE isbn: 978-3-642-24123-9 book_title: Software Engineering for Resilient Systems, Proc. of 3rd International Workshop. September 29-30, 2011 Geneva, Switzerland citation: 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 document_url: http://deploy-eprints.ecs.soton.ac.uk/315/1/serene2011_submission_14-final.pdf