A Formal Analysis Method For System Requirements Based On UML

Unified Modeling Language (UML is also called the standard Modeling Language) originates form an OMG standard in1997. UML is a graphical language which supports modeling and development of software systems. UML supports modeling and visualization for all stages of software development, including requirements, the specifications, the structure and the configuration. UML can add class-level constraints and system-level constraints, but there is no definition for the way to check the correctness of these constraints in the UML. Most specifications for UML are descriptive and easy to understand. But it is hard to verify the correctness of the constraints, for these specifications are not formal and short of precise semantics. To ensure the correctness of the system and to reduce the development costs and the operation risks, it is necessary to verify the safety of the system as early as possible. Especially the potential pitfalls in the requirements specification will have a significant impact on the development of the system. If those potential pitfalls cannot be found timely in the stage of system development, it would likely cause the fail of the system or even disastrous consequences.This paper is mainly about the formal analysis method for the analysis of the system requirements, and the UML specifications are verified through model checking. There is an automatic bump-shielded system with some specifications which have been used to show the process of formal verification. The UML model has been built by analyzing the requirements of the system and the class diagram, state diagram and sequence diagram are useful in this paper. The rules for the translation form UML diagrams to SMV program are put forward, and the tool to complete the translation as these rules is implemented in this paper. The model of system can be accepted by the NuSMV after the translation, so the performance of the system can be verified by NuSMV. The position, counter-example and other information of the errors which have been found will be displayed, which is convenient for the analysis and modification of the errors.The model for the requirements of the system is built by the Enterprise Architect, The verification of the system and the test to verify the effectiveness of the translation rules are also realized with Enterprise Architect. The experiment results show that the model-transformation method for the UML class diagram, UML state diagram and UML sequence diagram which originate from the system requirements is effective. Besides, the conversion process can be automated, which is more convenient for the formal verification.