21-25 May 2012
New York City, NY, USA
US/Eastern timezone

Applying formal verification methods to experiment triggers

24 May 2012, 13:30
4h 45m
Rosenthal Pavilion (10th floor) (Kimmel Center)

Rosenthal Pavilion (10th floor)

Kimmel Center

Poster Online Computing (track 1) Poster Session

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.

Primary author

Prof. Swain John (Noreastern University)

Co-authors

Prof. Gene Cooperman (Northeastern University) Prof. Pete Manolios (Northeatern University) Dr Thomas Paul (Northeastern University)

Presentation Materials

There are no materials yet.