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.
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)