梯形编程的自动演绎验证

• 2019 年 12 月 29 日
• 筆記

原文题目: Automated Deductive Verification for Ladder Programming

摘要： 梯形逻辑是IEC 61131-3标准化的编程语言，广泛应用于工业可编程控制器（PLC）的编程。PLC程序由输入（其值在运行时由工厂传感器给出）、输出（其值在运行时由工厂执行器给出）和从输入值计算输出值的逻辑表达式组成。由于梯形编程的图形化形式和典型工业程序的输入输出量，调试此类程序既费时又容易出错。在本文中，我们将介绍一个基于Why3的工具原型，该工具原型已实现，用于自动执行演绎验证，以便为梯形编程开发人员提供易于使用且功能强大的调试工具。

原文作者：Denis Cousineau（法国三菱电气欧洲研发中心），DavidMentré（法国三菱电气欧洲研发中心），Hiroaki Inoue（日本尼崎市三菱电机株式会社）

原文地址：https://arxiv.org/abs/1912.10629