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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Abrial, J.-R.: System study: Method and example (1999), www-lsr.imag.fr/B/Documents/ClearSy-CaseStudies/
Idani, A., Ledru, Y.: Dynamic Graphical UML Views from Formal B Specifications. Journal of Information and Software Technology 48(3), 154–169 (2006)
Idani, A., Ledru, Y.: Object Oriented Concepts Identification from Formal B Specifications. Journal of Formal Methods in System Design 30(3), 217–232 (2007)
Idani, A., Ledru, Y., Bert, D.: Derivation of UML Class Diagrams as Static Views of Formal B Developments. In: Lau, K.-K., Banach, R. (eds.) ICFEM 2005. LNCS, vol. 3785, pp. 37–51. Springer, Heidelberg (2005)
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)
Leuschel, M., Butler, M.: ProB: A Model Checker for B. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, pp. 855–874. Springer, Heidelberg (2003)
Sekerinski, E.: Graphical Design of Reactive Systems. In: Bert, D. (ed.) B 1998. LNCS, vol. 1393, pp. 182–197. Springer, Heidelberg (1998)
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)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Idani, A. (2009). UML Models Engineering from Static and Dynamic Aspects of Formal Specifications. In: Halpin, T., et al. Enterprise, Business-Process and Information Systems Modeling. BPMDS EMMSAD 2009 2009. Lecture Notes in Business Information Processing, vol 29. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-01862-6_20
Download citation
DOI: https://doi.org/10.1007/978-3-642-01862-6_20
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-01861-9
Online ISBN: 978-3-642-01862-6
eBook Packages: Computer ScienceComputer Science (R0)