UML Models Engineering from Static and Dynamic Aspects of Formal Specifications
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.
KeywordsFormal Method Class Diagram Building State Concrete State Open Building
Unable to display preview. Download preview PDF.
- 1.Abrial, J.-R.: System study: Method and example (1999), www-lsr.imag.fr/B/Documents/ClearSy-CaseStudies/
- 5.Laleau, R., Mammar, A.: An Overview of a Method and Its Support Tool for Generating B Specifications from UML Notations. In: 15th IEEE Int. Conference on Automated Software Engineering, pp. 269–272. IEEE CS Press, Los Alamitos (2000)Google Scholar
- 8.Snook, C., Butler, M.: U2B − A tool for translating UML-B models into B. In: Mermet (ed.) UML-B Specification for Proven Embedded Systems Design (2004)Google Scholar