Abstract
We present the notion of consistency relation in UML and B multi-view specifications. It is defined as a semantic relation between both views. It provides us with a sound basis to define the notion of development operator. An operator models a development step; it separates the design decisions from their expression in the specification formalisms. Operator correctness is defined as a property which guarantees that the application of an operator on a consistent specification state yields a consistent new state. An operator can be proven once and for all to be correct. A classical case-study, the Generalized Railroad Crossing (GRC), demonstrates how the different notions can be put in practice to provide specifiers with a realistic development model.
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.
Similar content being viewed by others
References
Attali, I., Courbis, C., Degenne, P., Fau, A., Fillon, J., Parigot, D., Pasquier, C., Coen, C.S.: SmartTools: a development environment generator based on XML technologies. In: XML Technologies and Software Engineering, Toronto, Canada. ICSE 2001, ICSE workshop proceedings (2001)
Attiogbé, C., Poizat, P., Salaün, G.: Integration of Formal Datatypes within State Diagrams. In: Pezzé, M. (ed.) FASE 2003. LNCS, vol. 2621, pp. 341–355. Springer, Heidelberg (2003)
Oxford(UK) B-Core(UK) Ltd. B-Toolkit User’s Manual (1996)
ClearSy, http://www.b4free.com/index.php
Houda, F., Merz, S.: Transformation de spécifications B en diagrammes UML. In: Proceedings of AFADL 2004, Besançon, Fr (2004)
Idani, A., Ledru, Y.: Object Oriented Concepts Identification from Formal B Specifications. In: 9th Int.Workshop on Formal Methods for Industrial Critical Systems (FMICS 2004), Linz, AT (2004)
Laleau, R., Polack, F.: A Rigorous Metamodel for UML Static Conceptual Modelling of Information Systems. In: Dittrich, K.R., Geppert, A., Norrie, M.C. (eds.) CAiSE 2001. LNCS, vol. 2068, pp. 402–416. Springer, Heidelberg (2001)
Ledang, H.: Traduction Systématique de Spécifications UML vers B. PhD thesis, LORIA -Université Nancy2, (November 2002)
Ledang, H., Souquières, J.: Modeling class operations in B: application to UML behavioral diagrams. In: ASE 2001: 16th IEEE International Conference on Automated Software Engineering. IEEE Computer Society, Los Alamitos (2001)
Ledang, H., Souquières, J.: Integrating Formalizing UML Behavioral Diagrams with B. Workshop on Integration and Transformation of UML models, Malàga (S) (2002)
Ledang, H., Souquières, J.: Integration of UML and B Specification Techniques: Systematic Transformation from OCL Expressions into B. In: Proceedings of APSEC 2002. IEEE Computer Society, Los Alamitos (2002)
Ledang, H., Souquières, J., Charles, S.: ArgoUML+B: Un outil de transformation systématique de spécifications UML vers B. In: Proceedings of AFADL 2003, Rennes, Fr (2003)
Marcano, R., Levy, N.: Transformation rules of OCL constraints into B formal expressions. In: Jürjens, Cengarle, Fernandez, Rumpe, and Sandner (eds.), Critical Systems Development with UML – Proceedings of the UML 2002 workshop, pp. 155–162 (2002)
Marcano, R., Levy, N.: Using B formal specifications for analysis and verification of UML/OCL models. In: Kuzniarz, L., Reggio, G., Sourrouille, J.L., Huzar, Z. (eds.) Workshop on Consistency Problems in UML-based Software Development. Workshop Materials, pp. 91–105 (2002)
Meyer, E.: Développements formels par objets: utilisation conjointe de B et d’UML. PhD thesis, LORIA -Université Nancy2, mars (2001)
Meyer, E., Souquières, J.: A systematic approach to transform OMT diagrams to a B specification. In: Wing, J.M., Woodcock, J.C.P., Davies, J. (eds.) FM 1999. LNCS, vol. 1708, p. 875. Springer, Heidelberg (1999)
Meyer, E., Souquières, J.: A systematic approach to transform OMT diagrams to a B specification. In: Wing, J.M., Woodcock, J.C.P., Davies, J. (eds.) FM 1999. LNCS, vol. 1708, p. 875. Springer, Heidelberg (1999)
Okalas Ossami, D., Souquières, J., Jacquot, J.-P.: Opérations de construction de spécifications multi-vues UML et B. In: Proceedings of AFADL 2004, Besançon, France, June 16-18, INRIA (2004)
OMG. Unified modeling language specification, version 1.5 (March 2003), available from http://www.omg.org
Parigot, D., Courbis, C.: avaible at, http://www-sop.inria.fr/smartool/
Schnoebelen, P., Bérard, B., Bidoit, M., Laroussine, F., Petit, A.: Vérification de logiciels -Techniques et outils du model-checking-. Paris,Vuibert (1999), ISBN 2- 7117-8646-3
Snook, C., Butler, M., Oliver, I.: Towards a UML profile for UML-B. Technical report, DSSE-TR-2003-3, Electronics and Computer Science, University of Southampton (2003)
Snook, C., Buttler, M.: U2B: a tool for combining UML and B, Avaible at http://www.ecs.soton.ac.uk/~cfs/U2Bdownloads/
STERIA. Manuel de référence du langage B. -ClearSy-, (November 1998)
Tatibouet, B., Hammad, A., Voisinet, J.-C.: From an abstract B specification to UML class diagrams. In: 2nd IEEE International Symposium on Signal Processing and Information Technology (ISSPIT 2002), pp. 5–10 (2002)
Tatibouet, B., Voisinet, J.-C.: Generating statecharts from B specifications. In: 16th International Conference Software & Systems Engineering and their applications (ICSSEA 2003), Paris, Fr (2003)
Tatibouet, B., Voisinet, J.C.: jBtools and B2UML: a plateform and a tool to provide a UML class diagram since a B specification. In: ICSSEA: 14th International Conference on Software and Systems Engineering and Their Applications, Paris (Fr), vol. 2 (2001)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ossami, D.D.O., Jacquot, JP., Souquières, J. (2005). Consistency in UML and B Multi-view Specifications. In: Romijn, J., Smith, G., van de Pol, J. (eds) Integrated Formal Methods. IFM 2005. Lecture Notes in Computer Science, vol 3771. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11589976_22
Download citation
DOI: https://doi.org/10.1007/11589976_22
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-30492-0
Online ISBN: 978-3-540-32240-5
eBook Packages: Computer ScienceComputer Science (R0)