Research Of B Formal Specification Based On UML Class Diagram

With the rapid development of the information technology, the application range of computer software system gradually extends to all areas of the society. Consequently, with the increasing size and complexity of software, the possibility of error also increases. The problem of how to ensure software quality and improve software reliability has been an open issue in the field of software engineering. The paper combines UML with B method to research and try to overcome the drawback of in formal development method of the description of the demand specification.Firstly, UML and B method were analyzed and researched respectively. Most of semi-formal UML is lack of precise semantic, which is liable to produce vague or ambiguous explanations for its inaccurate description of modeling. B method, based on strict mathematical theories, can provide strict mathematical basis for software developer with precise and unambiguous specification. Then, class diagram, chosen from the UML static state model, is main research object in the static model study, and to analyze the abstract syntax of class diagram modeling elements. UML class diagram modeling elements are formally described by formal specification language of B methods. Further to characterize the semantic of class diagram modeling elements, formal mapping rules are built between class diagram modeling elements and symbolic notation of B methods. The paper realizes the transformation from UML class diagram model to the B formal specification. Finally, it illustrates the ways and the applications of formal description of UML class diagram, which is based on B-Method through an example analysis of elevator control system. The paper continues to give animation and model checking on the resulted of formal models through the use of ProB, to verify the validity of the mapping rules proposed.Combining UML and B show that B method provides the accurate semantic reference for UML model diagram.On the other hand, we can use visual UML specification as a tool for building B specifications to alleviate the difficulties in the process of direct application of this method, to raise its practical role in software development.