问题框架中问题领域因果行为的形式化验证  

Formal Validation of Causal Behaviors of Problem Domains in Problem Frames Approach

作　　者：朱利鲁 李智[2] 

机构地区：[1]广西师范大学广西多源信息挖掘与安全重点实验室,桂林541004 [2]广西师范大学广西区域多源信息集成与智能处理协同创新中心,桂林541004

出　　处：《计算机科学》2015年第12期136-142,156,共8页Computer Science

基　　金：国家自然科学基金(61262004;61262005);广西自然科学基金(2012GXNSFCA053010);广西科学研究与技术开发计划项目(桂科合1347004-22);广西教育厅科研项目(201203YB023);广西多源信息挖掘与安全重点实验室开放基金(14-A-03-01);"八桂学者"工程专项经费资助

摘　　要：为问题框架中问题渐变所依赖的问题领域因果行为的确立提出一种形式化验证方法。为了对问题渐变过程中事件间的因果关系提供可验证的证据支持,简化问题表征的复杂度,进而提高计算机领域软件规约的可靠性,采纳了一种基于NuSMV语言的符号模型检验的形式化验证方法。该验证方法采用UML状态机表示问题领域内部状态变化的有限结构空间,用CTL公式描述问题域内状态之间的可达性性质,通过遍历有限结构状态机来检验CTL公式的正确性,筛选出具有因果关系的外部共享事件,为问题渐变提供有效的技术支持。This paper proposed a method of formally identifying and validating causal behaviors of problem domains, which are the basis of problem progression in the problem frames approach. A symbolic model checking method based on the NuSMV language was adopted in order to provide verifiable evidence of causal relationships between events which are useful in problem progression, reduce the complexity of problem representation,and increase the reliability of specifications of the computing machine. A UML state-chart is used to represent the finite space of internal state transitions of a critical domain. A CTL formula is used to describe the reachability of certain internal states of the domain. A series of causally-related events are identified through traversing all the possible paths of state-transition in the state chart to validate the correctness of the CTL formula, thus providing effective technical support to problem progression.

关 键 词：问题框架 关键问题领域 因果行为 符号模型检验 可达性 

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