| Formal Method, based on strict mathematical theories, can provide strict mathematical basis for software developers with its precise specifications. It occupies a significant place in improving software reliability. Solid mathematical basis and the ability to use strict mathematical symbols in compiling specifications are two requirements in the application of the method, which makes it hard for many developers. Furthermore, formal specification is indirect and poorly readable, which make it inconvenient in the communication with users. Hence, research and applications of formal method still confines in a very limited circle.UML is a kind of visualized graphic modelling language. With direct graphical notation, it can provide graphic specification for system, which has become a de-facto standard notation for describing analysis and design models of object-oriented software systems. However, lots of UML concepts have informal semantics, which makes users liable to produce vague and ambiguous explanations for its inaccurate description of modelling. Lack of accuracy also makes it inconvenient for instruments to verify the described specifications.The Formal Method can just compensate those disadvantages of UML. It is able to perform consistency examination and correctness analysis on the results of UML modelling. Furthermore, UML can alleviate the difficulties in the process of direct application of this method, thus raising its practical role in software development. It is very important significant to improve the reliability of software through combining formal method and UML.This dissertation choose B-Method as the formal method to convert UML diagrams to the corresponding B models on the basis of analyzing the feature of the UML model diagram. Firstly, B-Method has object-oriented feature, which makes the process of formalize the UML diagrams more direct and understandable. Secondly B-Method has a set of theoretical analytic methods and tools to remedy the model analysis and verification means of UML. Thirdly,B-Method covers a software process from specification to implementation.This dissertation mainly puts forward the modelling method of UML class diagram and state-chart diagram based on B-Method. The developer can model the system through combining class diagram and state-chart diagram, and translate these models to B-Method formal specification, constructing 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.At the end of the dissertation, it illustrates the way and the application of formal description of UML diagrams based on B-Method through an elevator system. The dissertation continues to give animation and model checking on the resulted formal models through the use of ProB. |
PDF Full Text Request