| Formal Methods (Formal Method) is based on rigorous mathematical foundation and can generate unambiguous, precise formal specification, enables software developers to have a rigorous mathematical foundation and plays a positive role in improving software reliability. Formal technical requires that developers have a certain mathematical basis; it needs to use the rigorous mathematical notation to describe specification, which causes the technical threshold for software developers. At the same time, the readability of formal specification is not strong; expression is not intuitive enough, which makes difficulties to communicate with the user. The reasons above limit the research and application of formal methods.UML (Unified Modeling Language) language thanks to the intuitive graphical notation for system modeling has been widely used as strong versatility in the software engineering industry standard. Many described UML concepts are based on non-formal semantics; so it is difficult to achieve a precise definition of the target model that may result in the expression of vagueness or ambiguity, thus increasing difficulty of the analysis and validation of formal specification.UML and formal method have complementary, formal methods can make up for the lack in UML precise semantics, and ensured the the consistency of the model of the system obtained by the needs analysis in the development process. Meanwhile, UML can broaden the field of application of formal methods to improve the effectiveness of formal methods in the software development process. In short, the combination of both has a significant positive significance in the field of software development.This article mainly aims at UML class diagram and state diagram, gives their conversions of the mapping between the UML semantics and the B method and Z specifications. First, the software developers rely on UML class diagrams and state diagrams to construct model, then, according to the proposed conversion framework, constructed the B and Z formal specification of the corresponding system, at last used the appropriate method for dynamic analysis, and then verifies the system through model checking and theorem proving.Finally, according to an elevator system instance and LR(1), specifically expounds the transformation framework between the UML model and B method and Z specification, and build experimental environment for the simulation of the example to verify the program’s feasibility and effectiveness by ProB and Z/EVES. |
PDF Full Text Request