GXW规范的结构化综合
计算机科学中的逻辑
2016-07-07 v3 软件工程
摘要
我们将线性时序逻辑 (LTL) 的 GXW 片段定义为综合安全关键应用嵌入式控制软件的基础。由于 GXW 包含了弱直到 (weak-until) 算子的使用，我们能够指定若干不同的可编程逻辑控制 (PLC) 问题，这些问题编译自工业训练集。针对 GXW 控制器规范，我们开发了一种综合一组同步通信的基于参与者 (actor) 的控制器的新方法。该综合算法通过递归 GXW 规范的结构来进行，并根据公式结构生成一组专用且同步通信的子控制器。在后续步骤中，2QBF 约束求解识别并尝试解决个体 GXW 规范之间的潜在冲突。这种 GXW 综合的结构化方法支持安全关键软件认证机制所要求的需求与生成控制代码之间的可追溯性。GXW 规范的综合处于 PSPACE，而全功能 LTL 综合为 2EXPTIME-完全。确实，我们的实验结果表明 GXW 综合可良好扩展到具有 20 个输入和输出端口及以上的工业规模控制综合问题。
引用
@article{arxiv.1605.01153,
title = {Structural Synthesis for GXW Specifications},
author = {Chih-Hong Cheng and Yassine Hamza and Harald Ruess},
journal= {arXiv preprint arXiv:1605.01153},
year = {2016}
}
备注
The long (including appendix) version being reviewed by CAV'16 program committee. Compared to the submitted version, one author (out of her wish) is moved to the Acknowledgement. (v2) Corrected typos. (v3) Add an additional remark over environment assumption and easy corner cases