Skip to Main content Skip to Navigation
Conference papers

UML models engineering from static and dynamic aspects of formal specifications

Akram Idani 1 
1 VASCO - Validation de Systèmes, Composants et Objets logiciels
LIG - Laboratoire d'Informatique de Grenoble
Abstract : While formal methods are focused on some particular parts of software systems, especially secure ones, graphical techniques are the most useful techniques to specify in a comprehensible way large and complex systems. In this paper we deal with the B method which is a formal method used to model systems and prove their correctness by successive refinements. Our goal is to produce graphical UML views from existing formal B specifications in order to ease their readability and then help their external validation. In fact, such views can be useful for various stakeholders in a formal development process: they are intended to support the understanding of the formal specifications by the requirements holders and the certification authorities; they can also be used by the B developers to get an alternate view on their work. In this paper, we propose an MDE framework to support the derivation of UML class and state/transition diagrams from B specifications. Our transformation process is based on a reverse-engineering technique guided by a set of structural and semantic mappings specified on a meta-level.
Document type :
Conference papers
Complete list of metadata
Contributor : Catherine Oriat Connect in order to contact the contributor
Submitted on : Friday, February 28, 2014 - 1:54:25 PM
Last modification on : Wednesday, July 6, 2022 - 4:20:28 AM




Akram Idani. UML models engineering from static and dynamic aspects of formal specifications. 14th International Conference on Exploring Modeling Methods for Systems Analysis and Design ; co-located with CaiSE'2009, Springer, LNBIP, 2009, Amsterdam, The, Netherlands. pp.237-250, ⟨10.1007/978-3-642-01862-6_20⟩. ⟨hal-00953588⟩



Record views