Skip to Main content Skip to Navigation
Reports

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 :
Reports
Complete list of metadata

https://hal.inria.fr/inria-00100224
Contributor : Publications Loria <>
Submitted on : Tuesday, September 26, 2006 - 10:15:44 AM
Last modification on : Friday, February 26, 2021 - 3:28:07 PM

Identifiers

  • HAL Id : inria-00100224, version 1

Collections

Citation

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⟩

Share

Metrics

Record views

136