一种基于场景的性质验证方法

• 作者: 刘万伟 卓琳 谭庆平
• 来源期刊: 计算机工程与科学
• 学科: 工学
• 关键词: 顺序图 状态图 场景 命题标记路径集 有穷命题线性时序逻辑
• 年，卷（期）: 2006,（4）
• 所属期刊栏目: 算法研究
• 页码范围: 56-59
• 页数: 4页
• 分类号: TP311.5
• 字数: 6363字
• 语种: 中文
• DOI: 10.3969/j.issn.1007-130X.2006.04.019

摘要

顺序图是UML中重要的语法机制,用于对系统的动态行为进行建模.但是,建模后模型是否满足某方面性质却很难检验.为此,我们提出了一种基于场景的性质验证方法.该方法首先把描述一个场景的顺序图以及相关的状态图综合成一个"命题标记路径集",把待验证的性质表示为有穷线性时序逻辑公式,然后利用"逆向标注"算法对其进行验证.转化及验证过程均可自动完成.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	谭庆平	国防科技大学计算机学院	50	929	16.0	29.0
2	卓琳	长沙大学计算机系	7	56	4.0	7.0
6	刘万伟	长沙大学计算机系	1	10	1.0	1.0