PVS-based consistency checking for UML class diagrams and sequence diagrams
Ping Chen · Systems engineering and electronics · 2004
The consistency checking between UML class diagrams and sequence diagrams is studied, and a PVS-based consistency checking approach is proposed. Firstly necessary conditions for deciding consistency is given and then the meta theory with PVS specification language is presented. To check consistency of UML model, the consistency checking is converted to a problem of theorem proving. Compared with other approaches, this technique involves more comprehensive factors, such as inheritance, associative relationship as well as visibility and pre-and post-conditions of class methods. It can mechanically analyze the consistency of UML model.