UML模型中并发对象的组合验证  

Compositional Verification of Concurrent Objects in UML Models

作　　者：董威[1] 王戟[1] 齐治昌[1] 

机构地区：[1]国防科技大学计算机学院

出　　处：《计算机科学》2005年第7期231-233,F004,共4页Computer Science

基　　金：国家自然科学基金(No.60303013);武汉大学软件工程国家重点实验室开放基金(No.SKLSE03-08)

摘　　要：本文在用层次自动机结构化表示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.

关 键 词：并发对象 UML模型 STATECHARTS 验证 组合 同步合成 模拟关系 对象系统 模型检验 状态爆炸 结构化 自动机 状态图 协同 

分 类 号：TP311.1[自动化与计算机技术—计算机软件与理论] TP311.132[自动化与计算机技术—计算机科学与技术]