Systematic Transformation Method from UML to Event-B挂网链接：SRP:

https://www.scirp.org/book/detailedinforofabook?bookid=3046

亚马逊：

https://www.amazon.com/dp/1649979126?ref=myi_title_dp

谷歌图书：

https://books.google.cn/books/about?id=MoEMEQAAQBAJ&redir_esc=y

挂网链接：SRP:

https://www.scirp.org/book/detailedinforofabook?bookid=3046

亚马逊：

https://www.amazon.com/dp/1649979126?ref=myi_title_dp

谷歌图书：

https://books.google.cn/books/about?id=MoEMEQAAQBAJ&redir_esc=y

Systematic Transformation Method from UML to Event-B 电子版 0606.pdf

Abstract

Since the emergence of software engineering in the late 1960 s, requirements analysis has always been an important theme of software development. In the process of software development, many people are needed to cooperate to ensure the stability and reliability of the software. According to the degree of formalization in the software development process, software engineering methods can be divided into three types: non-formal, semi-formal and formal. In object-oriented software development, UML has become a de facto modeling standard. However, although UML is intuitive and easy to understand and apply, it has inaccurate semantics, and UML is a semi-formal modeling language that cannot be formally verified. Event-B is a formal method based on a large number of mathematical predicate logic, which is accurate but difficult to understand and apply. Therefore, how to combine the advantages of UML diagrams and Event-B methods is the focus of research.

The previous methods are based on the transformation of UML scattered diagram to Event-B, and lack of systematic transformation method. The systematic transformation method can realize the unification of the elements in UML and the elements in Event-B. The general software system is a medium-sized system. The medium-sized system can be well expressed by using the four diagrams of use case diagram, class diagram, state diagram and sequence diagram. With the above four diagrams, the requirements acquisition, analysis, design and detailed design of the software life cycle can be fully expressed. Based on the requirements of immune system and elevator system, this paper uses Event-B formal method to model based on Rodin platform, and verifies the model with the help of the prover of Rodin platform. Through ProB animation simulation and iUML-B graphical front-end, the specific execution process and current state of elevator model events are shown. The following work is carried out:

Firstly, a conversion method from use case diagram to Event-B formal method is described, and the mechanism of cellular immunity in immune system is expounded. The use case diagram of cellular immunity is given. Based on Rodin platform, the immune model is modeled, and the use case diagram of cellular immunity is transformed into Event-B method, and the proof obligation generated in the model is relieved.

Secondly, the systematic transformation method from UML to Event-B is described. The transformation rules from UML use case diagram, class diagram, state diagram and sequence diagram to Event-B formal method are given, and the specific implementation process is given.

Thirdly, according to the transformation method mentioned above, this method is applied to the elevator model with high reliability and safety requirements. The elevator model is verified by using the internal prover provided in the Rodin platform and the external prover provided by Atelier B, etc.

Fourthly, with the help of the graphical front-end provided by iUML-B and the animation simulation function provided by ProB, the execution process of events in the dynamic simulation model is dynamically simulated, and the problems of deadlock and invariant violation in the model are eliminated to verify the feasibility and effectiveness of the conversion method.

In a word, the transformation method from the four diagrams of UML to Event-B and the application in the elevator control system with high safety and reliability requirements. Based on the research of this example, the feasibility and effectiveness of the UML to Event-B systematic transformation method are verified. The system transformation method from UML to Event-B is not only conducive to the precision of UML and the use of software practitioners, but also enhances the understandability of formal methods, which is conducive to the promotion and application of formal methods.

Key words: Event-B; Formal method; Immune model; Elevator model; ProB; iUML-B