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

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