论文中心
所在位置:首页 > 论文材料

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

  • 发布者:gaoning
  • 发布时间:2014/9/10
  • 浏览次数:

论文发表在“第十三届全国软件与应用学术会议(NASAC2014)”上。

论文摘要:本文针对问题框架中问题变换的目的,提出了形式化验证关键问题领域因果行为的方法。同时,为了对问题渐变过程中事件间的因果关系提供可验证的证据支持,简化问题表征的复杂度,进而提高计算机领域软件规约的可靠性,本文采纳了一种基于NuSMV语言的符号模型检验的形式化验证方法。该验证方法采用UML状态机表示关键问题领域内部状态变化的有限结构空间,用CTL公式描述关键问题域内状态之间的可达性性质,通过遍历有限结构状态机来检验CTL公式的正确性,筛选出具有因果关系的外部共享事件,为问题渐变提供有效的技术支持。