Formal Methods in EAST-RD11

The EAST application is a collaboration between CERN, Utrecht University, and AFRODITE Partners.

EAST's interest in the project is in using formal methods for the analysis and design of the second level trigger software system, and to investigate the production of ELLA and VHDL descriptions of custom hardware components from VDM++ specifications.

Extensive use of programable devices (general purpose micro processors and field programmable gate arrays) in the second level trigger gives the system the flexibility whereby it can be adapted to meet changing environmental conditions and unprecedented physics signatures. Because the filter introduces bias in the data and sits in the data critical path of an experiment, its function must be garanteed and predictable, and its implementation must be robust with respect to minor component failure. In addition, the system is likely to be implemented as a distributed asynchronous architecture capable of latency of a few microseconds. These requirements motivate our research into the use of formal methods in our application domain.

See formal methods in second-level trigger applications for papers relating to the EAST application

See also Global Second-Level Trigger case study.

Miscellaneous formal methods sources:

• Formal Methods
• Formal Method Sites
• VDM
• Z

' If language is not correct, then what is said is not what is
meant; if what is said is not what is meant, then what ought
to be done remains undone.' 
                       Great Sage Confucius (c.550-c.478 BC)