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
Type de document :
Rapport
[Intern report] A04-R-267 || truong04d, 2004, 20 p
Liste complète des métadonnées

https://hal.inria.fr/inria-00100224
Contributeur : Publications Loria <>
Soumis le : mardi 26 septembre 2006 - 10:15:44
Dernière modification le : jeudi 11 janvier 2018 - 06:20:08

Identifiants

  • 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〉

Partager

Métriques

Consultations de la notice

91