基于Coq的PLC语义形式化推理
On Formal Reasoning on the Semantics of PLC using Coq
摘要：
可编程逻辑控制器（PLC）及其编程标准IEC 61131-3广泛应用于工业自动化领域的嵌入式系统中。我们提出了一个框架的基础上，IEC 61131-3标准的PLC的正式治疗。PLC系统描述通常将以IEC 61131-3中定义的不同语言编写的代码组合在一起。对于顶层规范，我们认为顺序功能图（SFC）语言，图形高级语言，允许描述系统的主要控制流。除此之外，我们还描述了指令表（IL）语言--一种类似汇编的语言--以及另外两种图形语言：梯形图（LD）和功能框图（FBD）。IL、LD和FBD用于描述PLC的更低级别的结构。我们形式化这些语言的语义，并描述和证明它们之间的关系。使用证明助手Coq进行形式化和相关证明。除此之外，我们提出了一个工具，用于自动生成SFC表示从图形描述-IL和LD语言可以直接在Coq处理-及其使用验证的目的。我们素描可能的用途，我们的正式框架，并提出了一个例子应用程序的PLC在一个项目演示和证明安全性能。
英文摘要：
Programmable Logic Controllers (PLC) and its programming standard IEC 61131-3 are widely used in embedded systems for the industrial automation domain. We propose a framework for the formal treatment of PLC based on the IEC 61131-3 standard. A PLC system description typically combines code written in different languages that are defined in IEC 61131-3. For the top-level specification we regard the Sequential Function Charts (SFC) language, a graphical high-level language that allows to describe the main control-flow of the system. In addition to this, we describe the Instruction List (IL) language -- an assembly like language -- and two other graphical languages: Ladder Diagrams (LD) and Function Block Diagrams (FBD). IL, LD, and FBD are used to describe more low level structures of a PLC. We formalize the semantics of these languages and describe and prove relations between them. Formalization and associated proofs are carried out using the proof assistant Coq. In addition to this, we present work on a tool for automatically generating SFC representations from a graphical description -- the IL and LD languages can be handled in Coq directly -- and its usage for verification purposes. We sketch possible usages of our formal framework, and present an example application for a PLC in a project demonstrator and prove safety properties.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
