G4LTL-ST：PLC 程序的自动生成
计算机科学中的逻辑
2014-05-16 v2
摘要
G4LTL-ST 能够根据输入输出信号的时序行为规约，自动综合工业可编程逻辑控制器（PLC）的控制代码。这些规约采用线性时序逻辑（LTL）表达，并扩展了非线性算术约束和信号时序约束。G4LTL-ST 生成符合 IEC 61131-3 标准的结构化文本（Structured Text）代码，可编译为适用于大量工业现场级设备的可执行代码。G4LTL-ST 的综合算法实现了数据约束的伪布尔抽象以及时序约束到 LTL 的编译，并结合了反策略引导的抽象细化综合循环。由于时序逻辑规约在实践中 notoriously 难以使用，G4LTL-ST 通过根据失败的综合尝试建议对控制环境行为施加合适的限制，从而辅助工程师指定可实现的控制问题。
引用
@article{arxiv.1405.2409,
title = {G4LTL-ST: Automatic Generation of PLC Programs},
author = {Chih-Hong Cheng and Chung-Hao Huang and Harald Ruess and Stefan Stattelmann},
journal= {arXiv preprint arXiv:1405.2409},
year = {2014}
}
备注
This is the full version of the CAV'14 paper. Research concepts developed this paper are mainly from the technical report "Numerical LTL synthesis for cyber-physical systems", coauthored by Chih-Hong Cheng (ABB Research) and Edward A. Lee (UC Berkeley)