Automatic Formal Verification for EPICS

Jacky, Jonathan; Banerian, Stefani; Ernst, Michael; Loncaric, Calvin; Pernsteiner, Stuart; Tatlock, Zachary; Torlak, Emina

doi:10.18429/JACoW-ICALEPCS2017-TUDPL02

Joint Accelerator Conferences Website

The Joint Accelerator Conferences Website (JACoW) is an international collaboration that publishes the proceedings of accelerator conferences held around the world.

RIS citation export for TUDPL02: Automatic Formal Verification for EPICS

TY - CONF
AU - Jacky, J.P.
AU - Banerian, S.P.
AU - Ernst, M.D.
AU - Loncaric, C.A.
AU - Pernsteiner, S.
AU - Tatlock, Z.L.
AU - Torlak, E.
ED - Schaa, Volker RW
ED - Costa, Isidre
ED - FernÃ¡ndez, David
ED - Matilla, Ãscar
TI - Automatic Formal Verification for EPICS
J2 - Proc. of ICALEPCS2017, Barcelona, Spain, 8-13 October 2017
C1 - Barcelona, Spain
T2 - International Conference on Accelerator and Large Experimental Control Systems
T3 - 16
LA - english
AB - We built an EPICS-based radiation therapy machine control system, and are using it to treat patients at our hospital. To help ensure safety, we use a restricted subset of EPICS constructs and programming techniques, and developed several new automated formal verification tools for them. The Symbolic Evaluator checks properties of EPICS database programs (applications), using symbolic evaluation and satisfiability checking. It found serious errors in our control program that were missed by reviews and testing. Other tools are based on a formal semantics for database records, derived from EPICS documentation and expressed in the specification language of an automated theorem prover. The Verified Interpreter is a re-implementation of the parts of the database engine we use, which is proved correct against the formal semantics. We used it to check those parts of EPICS core by differential testing. It found no significant errors (differences between EPICS behavior and the formal semantics). A Verified Compiler is in development. It will compile a database to a standalone program that does not use EPICS core, where the machine code is verified to conform to the formal semantics.
PB - JACoW
CP - Geneva, Switzerland
SP - 285
EP - 291
KW - ion
KW - EPICS
KW - controls
KW - database
KW - operation
DA - 2018/01
PY - 2018
SN - 978-3-95450-193-9
DO - 10.18429/JACoW-ICALEPCS2017-TUDPL02
UR - http://jacow.org/icalepcs2017/papers/tudpl02.pdf
ER -