HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation

Boo - A formal approach to specification and verification of object-oriented system

Ninh Thuan Truong 1 Jeanine Souquières 1
1 DEDALE - Development of specifications
LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : The B notation is based on set theory, the language of generalised substitutions and first order logic. B specifications are composed of abstract machines whose states can be modified by operations. The rigour of B specifications is ensured by proof obligations which are automatically generated and proved by the B support tools. The mechanism of proof is based on mathematical reasoning and rules of inference. In this paper, we present a formal approach to specification and verification of an object-oriented system based on the B method. We lightly modify the structure of abstract machines to make it similar to classes in object-oriented notations. We introduce a simulation machine to simulate the execution and to check the correctness of a specified system. A case study is used to illustrate this approach
Document type :
Complete list of metadata

Contributor : Publications Loria Connect in order to contact the contributor
Submitted on : Tuesday, September 26, 2006 - 10:15:44 AM
Last modification on : Friday, February 26, 2021 - 3:28:07 PM


  • HAL Id : inria-00100224, version 1



Ninh Thuan Truong, Jeanine Souquières. Boo - A formal approach to specification and verification of object-oriented system. [Intern report] A04-R-267 || truong04d, 2004, 20 p. ⟨inria-00100224⟩



Record views