一种基于编码的OBDD模型检测的算法实现

An Algorithm of OBDD Model Checking Based on State Encoding

文章根据OBDD模型检测的基本思想并结合一个微波炉模型实例来介绍一种基于状态编码的OBDD模型检测算法实现。该算法实现通过介绍自行开发的OBDD模型检测器,具体描述了OBDD的生成、化简以及使用OBDD进行模型检测的具体实现算法以及OBDD模型检测的全过程,该算法实现简洁易读,可以直接应用于相关程序的开发。

This pager gives a realization process of OBDD model checking algorithm based on state encoding by means of introducing the basic idea of OBDD model checking in combination with a microwave oven model instance.Along with introducing the self-developed OBDD model checking detector,specific description of the OBDD generation,simplification,realization techniques and the whole checking process using OBDD are developed.The algorithm simple and easy to read,can be applied directly in the relevant program development.