基于 Coq 的 PLC 语义形式化推理

Jan Olaf Blech; Sidi Ould Biha

基于 Coq 的 PLC 语义形式化推理

软件工程 2013-01-15 v1 编程语言

作者: Jan Olaf Blech , Sidi Ould Biha

摘要

可编程逻辑控制器（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 的应用实例，同时证明了其安全性。

关键词

可编程逻辑控制器形式语义 Coq IEC 61131-3 验证

引用

@article{arxiv.1301.3047,
  title  = {On Formal Reasoning on the Semantics of PLC using Coq},
  author = {Jan Olaf Blech and Sidi Ould Biha},
  journal= {arXiv preprint arXiv:1301.3047},
  year   = {2013}
}

备注

arXiv admin note: text overlap with arXiv:1102.3529

基于 Coq 的 PLC 语义形式化推理

摘要

关键词

引用

备注

相关论文