Industrial deployment of system engineering methods providing high dependability and productivity


Use case scenarios as verification conditions: Event-B/Flow approach

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



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.

Item Type:Book Section
Tool developments
Tool developments > Model construction
Tool developments > Rodin plug-ins
ID Code:315
Deposited By: Prof A Romanovsky
Deposited On:04 Jul 2011 12:44
Last Modified:29 Oct 2011 18:28

Repository Staff Only: item control page

Deploy-Project - All right reserved