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

New Approach for Modeling State-Chart Diagrams in B

Hung Ledang 1 Jeanine Souquières 1
1 DEDALE - Development of specifications
LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : An appropriate approach for integrating UML and B specification techniques allows us to map UML specifications into B specifications. Therefore, we can formally analyze an UML specification via the corresponding B formal specification. This point is significant because B support tools are available. We can also use UML specifications as a tool for building B specifications. Thus, an approach for a practical and rigorous software development, which is based on object and B from the requirements elicitation to the executable code, is proposed. In this paper, we address the problem of modeling UML state-chart diagrams in B, which has not been, so far, completely treated. We distinguish between event-based and activity-based parts of state-chart diagrams. We propose creating, for each part, a B specification. Because activities relate to class operations, we can use our previous work on modeling class operation for modeling the activity-based part. Hence, we consider here only the event-based part. A new approach for modeling events is proposed. The asynchronous communication amongst state-chart diagrams is also considered.
Document type :
Complete list of metadata

Cited literature [14 references]  Display  Hide  Download

Contributor : Publications Loria Connect in order to contact the contributor
Submitted on : Thursday, October 19, 2006 - 9:00:48 AM
Last modification on : Friday, February 26, 2021 - 3:28:07 PM
Long-term archiving on: : Friday, November 25, 2016 - 12:47:16 PM


  • HAL Id : inria-00107544, version 1



Hung Ledang, Jeanine Souquières. New Approach for Modeling State-Chart Diagrams in B. [Intern report] A01-R-082 || ledang01f, 2001, 12 p. ⟨inria-00107544⟩



Record views


Files downloads