TitleAutomatic formal verification for EPICS
Publication TypeConference Paper
Year of Publication2017
AuthorsJacky J, Banerian S, Ernst MD, Loncaric C, Pernsteiner S, Tatlock Z, Torlak E
Conference NameICALEPCS 2017: 16th International Conference on Accelerator and Large Experimental Physics Control Systems
Date or Month PublishedOctober
Conference LocationBarcelona, Spain
AbstractWe 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. \par To check our control program, we built a \emphSymbolic 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. \par To check the EPICS runtime (EPICS Core) itself, we first developed a \emphFormal 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 \emphTrace 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 \emphVerified Compiler that could compile an EPICS database to a verified standalone program, while dispensing with much of the unverified EPICS toolchain and runtime.
Downloadshttps://www.youtube.com/watch?v=CFSnkB5z0GA talk video (YouTube)
Citation KeyJackyBELPTT2017