Formal verification is becoming more and more important in the production of high integrity microprocessors. The general purpose formal method called Event-B is the latest incarnation of the B Method: it is a proof-based approach with a formal notation and refinement technique for modelling and verifying systems. Refinement enables implementation-level features to be proven correct with respect to an abstract specification of the system. In this paper we demonstrate an initial attempt to model and verify Sandia National Laboratories' Score processor using Event-B. The processor is an (almost complete) implementation of a Java Virtual Machine in hardware. Thus, refinement-basedverification of the Score processor begins with a formal specification of Java bytecode.Traditionally,B has been directed at the formaldevelopment of software systems. The use of B in hardware verification could provide a means of developing combined software/hardware systems, i.e. codesign.
IOS Press, Inc.
6751 Tepper Drive
Clifton, VA 20124
Tel.: +1 703 830 6300
Fax: +1 703 830 2300 firstname.lastname@example.org
(Corporate matters and books only) IOS Press c/o Accucoms US, Inc.
For North America Sales and Customer Service
West Point Commons
Lansdale PA 19446
Tel.: +1 866 855 8967
Fax: +1 215 660 5042 email@example.com