kirancodes.me
To Proof Maintenance & Beyond!
ASE 2001

Modeling Class Operations in B: Application to UML Behavioral Diagrams

Hung Ledang, Jeanine Souquières

Full textDOI 10.1109/ase.2001.989815dblp

Abstract

An appropriate approach for translating UML to B formal specifications allows one to use UML and B jointly in a unified, practical and rigorous software development. We formally analyze UML specifications via their corresponding B formal specifications. This point is significant because B support tools like AtelierB are available. We can also use UML specifications as a tool for building B specifications, so the development of B specifications become easier In this paper we address the problem of automatic derivation from UML behavioral diagrams into B specifications, which has been so far an open issue. A new approach for modeling class operations in B is presented Each class operation is mapped into a B operation. A class operation and its involved data are mapped into the same B abstract machine (BAM). The class operation calling-called dependency is used to arrange derived B operations into BAMs. For each calling-called pair of class operations, the B operation of the called operation participates in the implementation of the B operation of the calling operation.

BibTeX
@inproceedings{Ledang-Souquieres:ASE01,
  author    = {Hung Ledang and
               Jeanine Souqui{\`{e}}res},
  title     = {Modeling Class Operations in B: Application to {UML} Behavioral Diagrams},
  booktitle = {ASE},
  pages     = {289--296},
  publisher = {{IEEE} Computer Society},
  year      = {2001},
}

Related papers