A method for the translation from UML into Event-B
| Autor: | Sun Weixuan, Fu Yangzhen, Feng Chao, Zhang Hong |
|---|---|
| Rok vydání: | 2016 |
| Předmět: |
Theoretical computer science
Use Case Diagram Computer science Communication diagram Applications of UML 02 engineering and technology computer.software_genre UML state machine Sequence diagram Unified Modeling Language Systems Modeling Language 020204 information systems 0202 electrical engineering electronic engineering information engineering Shlaer–Mellor method Use case Software system Formal verification Object Constraint Language computer.programming_language UML tool Programming language Computer Science::Software Engineering 020207 software engineering Class diagram Package diagram computer |
| Zdroj: | 2016 7th IEEE International Conference on Software Engineering and Service Science (ICSESS). |
| Popis: | The semi-formal language UML has become a standard notation for describing analysis and design models of complex software systems. But it's difficult to be verified formally. In order to solve this problem, a method to translate the UML models to the Event-B models has been proposed. The specific research is on the translation of the use case diagram and sequence diagram in UML. In the use case diagram, the users, the use cases and the relationship between them are taken into main consideration; In the sequence diagram, the objects of communication, the messages and the sending sequence of the messages are taken into main consideration. The translated models could be verificatied formally by the proof obligations in the platform of Rodin. Thus the purpose of formal verification for the semi-formal UML models has been achieved. Then the problem existing in the models could be found and the accuracy of the models could be guaranteed. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|