EXPERIENCE USING FORMAL METHODS IN HIGH-ENERGY PHYSICS

We report our experience using the formal method VDM(++) in high energ y physics realtime applications. VDM(++) is an extension of the establ ished formal method VDM to include object-oriented, concurrency and re al-time features. VDM(++) is supported by the VENUS tool-set, comprisi ng an OMT graphical editor, VDM(++) syntax and type checker, and a C+ code generator. Formal specification meta-languages allow formal data modeling, algorithm and system behavior specification at a highly abs tract level. Once an abstract design has converged it is refined towar ds a particular implementation, with formal validation of each step if desired. We have applied VDM(++) to the design of a fast track patter n recognition algorithm; the design of a global second- level trigger system for LHC experiments; the specification of simulated physics dat a; and the design of a data router hardware unit for a LHC second-leve l trigger. We are encouraged by the application of mathematics in an e ngineering discipline and conclude that formal methods have the potent ial to make a valuable contribution to the systems development process in high energy physics.