Home // PATTERNS 2014, The Sixth International Conferences on Pervasive Patterns and Applications // View article

Refinement Patterns for an Incremental Construction of Class Diagrams

Authors:
Boulbaba Ben Ammar
Mohamed Tahar Bhiri

Keywords: UML; OCL; refinement pattern; class diagram

Abstract:
Specifying complex systems is a difficult task, which cannot be done in one step. In the framework of formal methods, refinement is a key feature to incrementally develop more and more detailed models, preserving correctness in each step. Our objective is an incremental development, using the technique of refinement with proof for UML specifications. Indeed, UML suffers from two major weaknesses, namely, it is not based on a simple and rigorous mathematical foundation and it does not support the concept of refinement with proof of correction. To achieve this, we advocate a development framework combining the semi-formal features of UML/OCL and the formal one from B method. We chose the B formal language in order to benefit from existing work done on coupling between UML and B. In addition, we propose and formalize in B the refinement patterns that promote incremental development with proof of UML/OCL class diagrams. We illustrate our purpose by the description of some development steps of an access control system.

Pages: 50 to 59

Copyright: Copyright (c) IARIA, 2014

Publication date: May 25, 2014

Published in: conference

ISSN: 2308-3557

ISBN: 978-1-61208-343-8

Location: Venice, Italy

Dates: from May 25, 2014 to May 29, 2014