%0 Journal Article
%T umlstatecharts的模型检验方法
%A 董威？
%A 王戟？
%A 齐治昌？
%J 软件学报
%P 750-756
%D 2003
%X 统一建模语言uml已广泛应用于软件开发中,验证uml模型是否满足某些关键性质成为一个重要问题.提出了对umlstatecharts进行模型检验的方法.首先用扩展层次自动机结构化地表示umlstatecharts,然后给出其操作语义,通过寻找最大无冲突迁移集可以保证语义的正确性.对于具有无穷运行的系统,该操作语义可以映射到一个büchi自动机.使用基于自动机理论的模型检验方法来验证umlstatecharts的线性时态逻辑性质,并给出方法验证由statecharts和协同图建模的复杂多对象系统.
%K uml(unified
%K modeling
%K language)
%K statecharts
%K 模型检验
%K ω自动机
%U http://www.jos.org.cn/ch/reader/view_abstract.aspx?file_no=20030405&flag=1