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
|
PDF
651Kb |
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.
Item Type: | Book Section |
---|---|
Subjects: | Event-B Methodology 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