SRI Logo
About Us|R and D Divisions|Careers|Newsroom|Contact Us|SRI Home
     
  SRI Logo

PBS: Support for the B-Method in PVS
 by César Muñoz.

Abstract
The B-method is a state-oriented formal method for software development. It provides a uniform language, the abstract machine notation, to specify, design, and implement systems. The underlying logic of the method is a set theory with a first-order predicate calculus, On the other hand, PVS is a specification language integrated with a theorem prover. The logical framework of PVS is a higher-order logic with a type system. PVS does not come with a particular built-in software construction methodology. We show how the abstract machine notation of the B-method can be supported by PVS. We advocate a shallow embedding, but rather than translate the abstract machine notation in PVS, we add the notation as a layer over the PVS language. The embedding has been fully implemented in a front-end tool called PBS.
Files
 













 

About Us  |  R&D Divisions  |  Careers  |  Newsroom  |  Contact Us
© 2017 SRI International 333 Ravenswood Avenue, Menlo Park, CA 94025-3493
SRI International is an independent, nonprofit corporation. Privacy policy