16-23 September 2016
Oak Ridge National Laboratory
US/Eastern timezone

Automatic Formal Verification for EPICS

22 Sep 2016, 15:50
20m
Conference Center (Oak Ridge National Laboratory)

Conference Center

Oak Ridge National Laboratory

Building 5200 Oak Ridge National Laboratory Oak Ridge, TN 37831 USA
Regular Talk (15min) Other EPICS Collaboration Meeting

Speaker

Jonathan Jacky (University of Washington Medical Center)

Description

The Clinical Neutron Therapy System (CNTS) is a unique cyclotron-based radiation therapy machine at the University of Washington Medical Center. CNTS uses EPICS in its control system. This is a safety-critical medical application so we have undertaken a research project to supplement our usual software quality assurance by formal verification. The project includes an intensive review, analysis, and re-implementation of parts of EPICS. Several tools are under development. The EPICS Symbolic Evaluator automatically checks properties of an EPICS database. It either confirms the property or provides a counterexample. The EPICS Verified Interpreter is a re-implementation of the EPICS database engine, proved correct with an automated theorem prover, and validated by automated differential testing against an EPICS IOC. The EPICS Verified Compiler will compile an EPICS database to a standalone program that replaces the present EPICS runtime with a smaller trusted core.

Primary author

Jonathan Jacky (University of Washington Medical Center)

Co-authors

Calvin Loncaric (University of Washington Department of Computer Science) Prof. Emina Torlak (University of Washington Department of Computer Science) Prof. Michael Ernst (University of Washington Deparment of Computer Science) Stefani Banerian (University of Washington Medical Center) Stuart Pernsteiner (University of Washington Department of Computer Science) Prof. Zachary Tatlock (University of Washington Department of Computer Science)

Presentation Materials