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)
