Study On Translating UML To B Systematically Based On Unified Process

At present, the software industrial community is faced with double pressure: the function of the products become more and more complex and the cycle of producing products become shorter and shorter. The aim of software engineering is that we can still produce correct and reliable system when the complexity of the software is increased. Formal method is one of the ways to achieve the goal. Formal method is efficient way which is used for requirement analyzing,designing and validating when developing software systems. It is based on mathematics, and includes various languages,techniques and tools. When we use formal method to develop systems step by step, the reliability and productivity of software can be improved, and software automation can be implemented.The Unified Modeling Language (UML) has become a de-facto standard notation for describing analysis and design models of object-oriented software systems. But it has some shortages in some aspects. First, UML is only one kind of modeling language, but not a method. So when we develop an actual system, a specific process technique is required. Second, modeling of complex systems requires rigorous analysis of semantics, but UML is lack of rigorous semantics, so it is difficult to verify and analyze UML specifications. This point is considered as a serious drawback of UML-based technique.To overcome the problem mentioned above, this thesis proposes thought of formalizing UML based on the Unified Process. It also integrates RUP, UML and formal method to model software systems. Among them, UML is used as a language for modeling, the graphical description of models is easily accessible; RUP which integrates with UML is used as a supervising method, the integration can make the analysis and designing of a system more clear, and reduce risk of developing systems; The study of formal semantics transition of UML can enhance the accuracy,consistency and expansibility of this language. Then we can provide a theoretical method for the validation,transition and consistency checking of the model.This thesis introduces one of the mature formal methods--- B method. Compared to other formal methods, B method has many advantages:B is a formal software development method that covers a software process from specification,design to implementation. Furthermore, B method is supported by some tools such as Atelier-B,B-Toolkit and ProB.This thesis mainly discusses the transition of the use case diagram, class diagram,and sequence diagram in UML to B. It also discusses an extension of translating UML state chart to B so that the techniques can be suitable for some special cases. Following the theory of Unified Process, software developers can model the object-oriented system with UML, then translate them into B formal specification. Thereby we can map semi-formal model with diagrams and text to formal model based on mathematics. On this basis, the model checking,proof obligation and validation semi-automatic generating of code can be further implemented.At the end of the thesis, we illustrate the way and the application of formal description of UML diagrams systematically based on B-Method through an immune system, then continue to give animation and model checking on the resulted formal models through the use of ProB to make the validity and reliability of the specification.