有限状态系统检验的仿真方法

摘要

在软硬件系统的模型检验中经常需要检测系统模型和规约模型的行为之间的包含关系．为提高模型检验技术的自动化程度，提出一种针对有限状态机的仿真检验方法．首先在有限状态系统的基础上，提出系统及其外部行为的概念，然后定义了系统间的仿真关系，之后结合不动点定理，设计了和仿真关系定义相似的FP算子，这就把两个系统外部行为之间的包含关系转化为通过FP寻找组合系统间的最大不动点．如最大不动点存在，称系统模型满足规约属性．最后，通过等价关系给出一种对于无限状态系统转换成有限状态系统的方法，使得该方法可同样应用于无限状态系统．实例显示，该方法能够很好地满足模型检验的要求．