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.
展开▼
