Boo - A formal approach to specification and verification of object-oriented system - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Rapport Année : 2004

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

Résumé

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
Fichier non déposé

Dates et versions

inria-00100224 , version 1 (26-09-2006)

Identifiants

  • HAL Id : inria-00100224 , version 1

Citer

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⟩
79 Consultations
0 Téléchargements

Partager

Gmail Facebook X LinkedIn More