Paper Details

@InProceedings{GrantEvans07,
  title = "{T}owards the {F}ormal {V}erification of a {J}ava {P}rocessor in {E}vent-{B}",
  author= "Grant, Neil and Evans, Neil",
  editor= "McEwan, Alistair A. and Schneider, Steve and Ifill, Wilson and Welch, Peter H.",
  pages = "425--442",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2007",
  isbn= "978-1-58603-767-3",
  year= "2007",
  month= "jul",
  abstract= "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-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.