Compositional Verification of Concurrent Objects in UML Models
UML模型中并发对象的组合验证

Based on expressing UML Statecharts with hierarchical automata structurally, the paper defines the syn- chronous composition of concurrent objects in UML collaboration diagram. Then, the method and rules of composi- tional verification for concurrent object systems are studied based on the simulation relation between structures, which makes it possible that the global state graph is not needed in model checking and state explosion problem will be reduced.