Automatic Formal Verification for EPICS

Automatic Formal Verification for EPICS
复制标题

EPICS 的自动形式验证

DOI：
10.18429/jacow-icalepcs2017-tudpl02
复制
发表时间：
2018
期刊：
ArXiv
影响因子：
--
通讯作者：
Emina Torlak
Emina Torlak
中科院分区：
--
文献类型：
--
作者：
J. Jacky;S. Banerian;Michael D. Ernst;Calvin Loncaric;Stuart Pernsteiner;Zachary Tatlock;Emina Torlak

文献摘要

被引文献

相似文献

我们构建了基于 EPICS 的放射治疗机控制程序，并使用它来治疗我们医院的患者。为了帮助确保安全，控制程序使用 EPICS 构造和编程技术的受限子集，并且我们为此子集开发了几种新的自动化形式验证工具。为了检查我们的控制程序，我们构建了一个符号解释器，它使用符号执行和可满足性检查来查找 EPICS 数据库程序中的错误。它在我们的控制程序中发现了审查和测试中遗漏的严重错误。为了检查 EPICS 运行时（EPICS 核心）本身，我们首先基于 EPICS 记录参考手册（RRM）开发了 EPICS 数据库程序的形式语义，并用自动定理证明器的规范语言表示。我们构建了一个经过正式验证的跟踪验证器，并使用它通过对数百万个随机生成的程序进行差异测试来根据我们的语义检查 EPICS 运行时。测试过程总体上证实了EPICS运行时符合RRM中的规范，但确实发现RRM中的一些遗漏和模糊之处可能会误导用户。我们的 EPICS 形式语义支持有价值的未来开发：我们的 EPICS 程序正确性的完整证明、对任意 EPICS 程序的经过验证的分析，以及可以将 EPICS 数据库编译为经过验证的独立程序的经过验证的编译器，同时省去了许多未经验证的 EPICS 工具链和运行时。
We built an EPICS-based radiation therapy machine control program and are using it to treat patients at our hospital. To help ensure safety, the control program uses a restricted subset of EPICS constructs and programming techniques, and we developed several new automated formal verification tools for this subset. To check our control program, we built a Symbolic Interpeter that finds errors in EPICS database programs, using symbolic execution and satisfiability checking. It found serious errors in our control program that were missed by reviews and testing. To check the EPICS runtime (EPICS Core) itself, we first developed a Formal Semantics for EPICS database programs, based on the EPICS Record Reference Manual (RRM) and expressed in the specification language of an automated theorem prover. We built a formally-verified Trace Validator and used it to check the EPICS runtime against our semantics by differential testing with millions of randomly generated programs. The testing process generally corroborated that the EPICS runtime conforms to its specification in the RRM, but it did find several omissions and ambiguities in the RRM that might mislead users. Our formal semantics for EPICS enables valuable future developments: a full proof of correctness for our EPICS program, verified analyses for arbitrary EPICS programs, and a Verified Compiler that could compile an EPICS database to a verified standalone program, while dispensing with much of the unverified EPICS toolchain and runtime.