可编程逻辑控制器的验证方法

本文提出了一种用于验证可编程逻辑控制器的迭代方法。 我们探索了系统中的时序，环境和控制器逻辑的建模方法，其中采用了谓词抽象和反例指导的优化策略。 我们使用一个有代表性的示例来说明所提出的方法，并通过模型检查器CBMC对其进行验证。 实验结果证明了该方法的有效性。