The Research On B Formal Specification Of UML Use Case Model

With rapid development of information technology,the application range of compute software system gradually extended to all areas of society. Consequently, as the size and complexity of software increasing, 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. Integrating formal methods and mainstream software development methods is a feasible approach.UML is a kind of popular visual modeling language, has become a de facto industry standard notation for describing analysis and design models of object-oriented software systems. UML model is characterized by an intuitive, easy to understand, it is conducive to communication between developer and users. However, Most of UML semantics is described using natural language, lack of precise semantic, which makes users liable to produce vague or ambiguous explanations for its inaccurate description of modeling.Furthermore, UML lack of effective reasoning mechanism and perfect capacity of model checking also make it inconvenient for instruments to dynamic analysis and verify the described specification.Formal Method, based on strict mathematical theories, can provide strict mathematical basis for software developer with precise and unambiguous specification. It occupies a significant place in improving software reliability. Nevertheless, formal specification is indirect and poorly readable, which make it inconvenient in the communication with users. Hence, research and application of formal method still confines in a very limited circle. From those it can be seen that the combination of both formal method and UML will have complementary advantages. That is a very important significant to assuarance the quality and improve the reliability of software.This dissertation chooses B-Method as formal method. The appropriate approach for integrating UML and B specification techniques would allow us to map UML specifications into B specifications. Therefore, on the one hand, we can formally analyze correctness and check consistency an UML specification via the corresponding B specification. This point is significant because B support tools are available. On the other hand, we can use UML specification as a tool for building B specifications. It is can alleviate the difficulties in the process of direct application of this method, thus raising its practical role in software development.In this dissertation, by taking use case model as main research object. On this basis of analyzing the concepts of UML use case model and B abstract machine notion, describes the abstract syntax of use case modeling elements, creates a mapping between the two, realize the transformation from UML use case model to the B formal specification. In the first instance, Software developer model requirement models of the target system by using semi-formal UML use case model, then translate the this models to B formal specification according to the given method, construct formal specification of the system, and make use of B-Method supported tool to animation and prove the specification, which gets a reliable specification, as a correct beginning of formal reason and refinement.Finally, it illustrates the way and the application of formal description of UML use case model based on B-Method through an example analysis of elevator control system. The dissertation continues to give animation and model checking on the resulted formal models through the use of ProB.