-
题名问题框架中问题领域因果行为的形式化验证
被引量：1
- 1
-
-
作者
朱利鲁
李智
-
机构
广西师范大学广西多源信息挖掘与安全重点实验室
广西师范大学广西区域多源信息集成与智能处理协同创新中心
-
出处
《计算机科学》
CSCD
北大核心
2015年第12期136-142,156,共8页
-
基金
国家自然科学基金(61262004
61262005)
+4 种基金
广西自然科学基金(2012GXNSFCA053010)
广西科学研究与技术开发计划项目(桂科合1347004-22)
广西教育厅科研项目(201203YB023)
广西多源信息挖掘与安全重点实验室开放基金(14-A-03-01)
"八桂学者"工程专项经费资助
-
文摘
为问题框架中问题渐变所依赖的问题领域因果行为的确立提出一种形式化验证方法。为了对问题渐变过程中事件间的因果关系提供可验证的证据支持,简化问题表征的复杂度,进而提高计算机领域软件规约的可靠性,采纳了一种基于NuSMV语言的符号模型检验的形式化验证方法。该验证方法采用UML状态机表示问题领域内部状态变化的有限结构空间,用CTL公式描述问题域内状态之间的可达性性质,通过遍历有限结构状态机来检验CTL公式的正确性,筛选出具有因果关系的外部共享事件,为问题渐变提供有效的技术支持。
-
关键词
问题框架
关键问题领域
因果行为
符号模型检验
可达性
-
Keywords
Problem frames, Critical problem domain, Causal behavior, Symbolic model checking, Reachability
-
分类号
TP311
[自动化与计算机技术—计算机软件与理论]
-
