Speaker
Prof.
Swain John
(Noreastern University)
Description
Modern particle physics experiments use short pieces of
code called ``triggers'' in order to make rapid decisions about whether incoming
data represents potentially interesting physics or not. Such decisions are
irreversible and while it is extremely important that they are
made correctly, little use has been made in the community of formal verification
methodology.
The goal of this research is to determine both a restricted language for writing software triggers and a formal verification methodology that can be learned by non-experts in time similar to what they would invest to learn a new programming language. That methodology will also include a more formal specification for the software triggers.
We describe domain-specific languages for preparing software triggers and their properties. These languages will be specified in ACL2, a theorem proving system that was awarded the ACM Software System Award, and has been used in industry to prove some of the most complex theorems ever proved about commercial systems. We develop libraries of definitions and theorems to significantly automate the testing, validation, and verification of software triggers.
This work will provide a bridge technology to allow physicists to
produce reliable software triggers. The burden of using a restricted
language is not large, since the software trigger programs are short.
Hence, the formal verification methodology and the need for a restricted
programming language represent a modest burden to the physicists.
This burden is considered a bargain in exchange for the greater software
reliability in triggers that will be the outcome of this work.
Summary
We apply methods of formal verifications to trigger software as a means to ensure higher software quality for short, critical pieces of code.
Author
Prof.
Swain John
(Noreastern University)
Co-authors
Prof.
Gene Cooperman
(Northeastern University)
Prof.
Pete Manolios
(Northeatern University)
Dr
Thomas Paul
(Northeastern University)
