WoTUG - The place for concurrent processes

Paper Details


%T Towards the Formal Verification of a Java Processor in Event\-B
%A Neil Grant, Neil Evans
%E Alistair A. McEwan, Steve Schneider, Wilson Ifill, Peter H. Welch
%B Communicating Process Architectures 2007
%X 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\[rs] Score processor using
   Event\-B. The processor is an (almost complete)
   implementation of a Java Virtual Machine in hardware. Thus,
   refinement\-based verification of the Score processor begins
   with a formal specification of Java bytecode. Traditionally,
   B has been directed at the formal development of software
   systems. The use of B in hardware verification could provide
   a means of developing combined software/hardware systems,
   i.e. codesign.


If you have any comments on this database, including inaccuracies, requests to remove or add information, or suggestions for improvement, the WoTUG web team are happy to hear of them. We will do our best to resolve problems to everyone's satisfaction.

Copyright for the papers presented in this database normally resides with the authors; please contact them directly for more information. Addresses are normally presented in the full paper.

Pages © WoTUG, or the indicated author. All Rights Reserved.
Comments on these web pages should be addressed to: www at wotug.org

Valid HTML 4.01!