| With the rapid development of computer technology, the software systems have become more and more sophisticated. By stratifying the complicated problem for a better solution, the modeling technique has turned out to be the best way to abstract the system. Arisen in the 90's of last century, the UML, based on the object-oriented technology, has developed as the standard modeling language and thus been used widely. Advanced in modeling from multi-aspect of system using single as well as integrated expression methods, UML can be adopted to describe both static structures and dynamic behaviors of a given system. However, there existing a certain amount of information redundancy and cross-interleaving among models corresponding to each aspect of the resulted representation system, there arise more and more consistency problems between UML models.As representative of formal verification techniques, model checking has been quite mature since its appearance from 80's of last century, highlight of which is the ability of transferring the system verification problem into a mathematical one. This technique is used to verify whether a product or design accords with either all or part of its specifications by mathematical reasoning and has been applied to implementing high dependable software and systems.This thesis studies how to apply the model checking technique based on automata theory to verifying the consistency among UML models and proposes a new consistency-verifying approach for the statechart diagrams and sequence diagrams. We show the consistency problems among UML models and interpret the model checking technologies based on automata theory in detail. In the processing of state diagrams as well as sequence diagrams, especially the sequence diagrams, we describe its semantic firstly, and then convert sequence diagrams into a set of LTL formulas according to its own semantic. So we can make Büchi automata theory successfully applied to consistency verifying field. |
PDF Full Text Request