摘要
本文在用层次自动机结构化表示UML Statecharts的基础上,定义了UML协同图中并发对象的同步合成,然后根据结构间的模拟关系,研究了对并发对象系统进行组合验证的方法和规则,使有可能在对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.
出处
《计算机科学》
CSCD
北大核心
2005年第7期231-233,F004,共4页
Computer Science
基金
国家自然科学基金(No.60303013)
武汉大学软件工程国家重点实验室开放基金(No.SKLSE03-08)
