Colin Snook
Abstract
The emergence of the UML as a de facto standard for object-oriented modeling has been mirrored by the success of the B method as a practically useful formal modeling technique. The two notations have much to offer each other. The UML provides an accessible visualization of models facilitating communication of ideas but lacks formal precise semantics. B, on the other hand, has the precision to support animation and rigorous verification but requires significant effort in training to overcome the mathematical barrier that many practitioners perceive. We utilize a derivation of the B notation as an action and constraint language for the UML and define the semantics of UML entities via a translation into B. Through the UML-B profile we provide specializations of UML entities to support model refinement. The result is a formally precise variant of UML that can be used for refinement based, object-oriented behavioral modeling. The design of UML-B has been guided by industrial applications.
- Abrial, J. R. 1996. The B Book---Assigning Programs to Meanings. Cambridge University Press, NY.]] Google Scholar
- Amey, P. 2004. Dear sir, yours faithfully: an everyday story of formality, In Practical Elements of Safety: Proceedings of the twelfth Safety-Critical Systems Symposium, Birmingham, UK, February, F. Redmill and T. Anderson, Eds. Springer-Verlag, London, 3--15.]]Google Scholar
- B-Core 1996. B-Toolkit User's Manual, Release 3.2. B-Core(UK) Ltd., Oxford, UK.]]Google Scholar
- Clarke, E. M., Grumberg, O., and Peled, D. 1999. Model Checking. MIT Press, Cambridge, MA.]] Google Scholar
- Clearsy 2003. AtelierB User Manual V3.6. ClearSy System Engineering, Aix-en-Provence, F.]]Google Scholar
- Clearsy 2000. AtelierB Training Course Level 2. ClearSy System Engineering, Aix-en-Provence, F.]]Google Scholar
- Craigen, D., Gerhart, S., and Ralston, T. 1995. Formal methods reality check: Industrial usage. IEEE Trans. Softw. Eng. 21, 2, 90--98.]] Google Scholar
- Facon, P., Laleau, R., and Nguyen, H. P. 1996. Mapping object diagrams into B specifications. In Methods Integration Workshop, Electronic Workshops in Computing (eWiC), Leeds, UK, March. Springer-Verlag.]]Google Scholar
- Facon, P., Laleau, R., Nguyen, H. P., and Mammar, A. 1999. Combining UML with the B Formal Method for the Specification of Database Applications. Research report, CEDRIC Laboratory, Paris, F.]]Google Scholar
- Glass, R. 2004. The mystery of formal methods disuse. Comm. ACM 47, 8, 15--17.]] Google Scholar
- Harel, D. 1987. Statecharts: A visual formalism for complex systems. Sci. Comput. Prog. 8, 3, 231--274.]] Google Scholar
- Lano, K., Clark, D., and Androutsopoulos, K. 2004. UML to B: Formal Verification of Object-Oriented Models. In Integrated Formal Methods, 4th International Conference, IFM 2004, Canterbury, UK, April 2004, E. A. Boiten, J. Derrick and G. Smith, Eds. Lecture Notes in Computer Science Vol. 2999, Springer-Verlag, Berlin Heidelberg, 187--206.]]Google Scholar
- Ledang, H. and Souquières, J. 2001. Integrating UML and B specification techniques. In Informatik 2001 Workshop on Integrating Diagrammatic and Formal Specification Techniques. Vienna, Austria, September. GI Jahrestagung (1) 2001, 641--648.]]Google Scholar
- Leuschel, M. and Butler, M. 2003. ProB: A Model-Checker for B, In Proceedings of Formal Methods Europe, FME 2003, Pisa, Italy, A. Keijiro, S. Gnesi and M. Dino, Eds. Lecture Notes in Computer Science Vol. 2805, Springer-Verlag, Berlin Heidelberg, 855--874.]]Google Scholar
- Matisse 2003. Methodologies and Technologies for Industrial Strength Systems Engineering (MATISSE) IST Programme RTD Research Project IST-1999-11435. 1 May 2000 to 28 February 2003 http://www.matisse.qinetiq.com/]]Google Scholar
- Mermet, J. (Ed.) 2004. UML-B Specification for Proven Embedded Systems Design. Kluwer Academic Publishers, Dordrecht, The Netherlands.]]Google Scholar
- Meyer, E. and Souquières, J. 1999. A systematic approach to transform OMT diagrams to a B specification. In World Congress on Formal Methods in the Development of Computing Systems, FM'99, Vol. I. Toulouse, France, September 1999, J. Wing, J. Woodcock and J. Davies, Eds. Lecture Notes in Computer Science, Vol. 1708, Springer-Verlag, Berlin Heidelberg, 875--895.]] Google Scholar
- Nagui-Raiss, N. 1994. A formal software specification tool using the entity-relationship model. In 13th International Conference on the Entity-Relationship Approach. Manchester, U.K., December, P. Loucopoulos, Ed. Lecture Notes in Computer Science, Vol. 881, Springer-Verlag, 315--332.]] Google Scholar
- Rumbaugh, J., Jacobson, I., and Booch, G. 1998. The Unified Modeling Language Reference Manual. Addison-Wesley, Reading, MA.]] Google Scholar
- Sekerinski, E. 1998. Graphical design of reactive systems. In B'98: Recent Advances in the Development and Use of the B Method---2nd International B Conference. Montpellier, France, April 1998, D. Bert, Ed. Lecture Notes in Computer Science, Vol. 1393, Springer-Verlag, 182--197.]] Google Scholar
- Shore, R. 1996. Object-oriented modelling in B. In Proceedings of the 1st Conference on the B method. Nantes, France, November, H. Habrias, Ed. 133--154.]]Google Scholar
- Snook, C., Oliver, I., and Butler, M. 2004. The UML-B profile for formal systems modelling in UML, In UML-B Specification for Proven Embedded Systems Design, J. Mermet, Ed. Kluwer Academic Publishers, Dordrecht, The Netherlands.]]Google Scholar
- Snook, C. and Butler, M. 2004. U2B---A tool for translating UML-B models into B, In UML-B Specification for Proven Embedded Systems Design, J. Mermet, Ed. Kluwer Academic Publishers, Dordrecht, The Netherlands.]]Google Scholar
- Snook, C., Tsiopoulos, L., and Waldén, M. 2003. A case study in requirement analysis of control systems using UML and B, In Proceedings of RCS'2003 International Workshop on Refinement of Critical Systems: Methods, Tools and Experience. Turku, Finland, June.]]Google Scholar
- Spivey, J. M. 1988. Understanding Z a specification language and its formal semantics. Cambridge University Press, NY.]] Google Scholar
- Toval, A., Requena, A., and Alemán, J. L. 2003. Emerging OCL Tools. Software and System Modeling (SoSyM), 2, 40, 248--261.]]Google Scholar
- Vaziri, M. and Jackson, D. 1999. Some shortcomings of OCL, the Object Constraint Language of UML. Response to Object Management Group's Request for Information on UML 2.0. Available at http://sdg.lcs.mit.edu/cdnj/publications.]]Google Scholar
- Voros, N., Snook, C., Hallerstede, S., and Masselos, K. 2004. Embedded System Design Using Formal Model Refinement: An Approach Based on the Combined Use of UML and the B Language, Design Automation for Embedded Systems 9, 2, 67--99.]]Google Scholar
- Warmer, J. and Kleppe, A. 2003. The Object Constraint Language Second Edition: Getting your models ready for MDA. Addison-Wesley.]] Google Scholar
Index Terms
- UML-B: Formal modeling and design aided by UML
Recommendations
A proposal for extending UML-B to support a conceptual model
UML-B is a development process framework for Event-B based on a "UML-like" graphical formal notation that provides support for object-oriented modelling concepts, in particular, for class and state machine diagrams. However, this methodology has a gap ...
A method of refinement in UML-B
UML-B is a `UML-like' graphical front-end for Event-B that provides support for object-oriented and state machine modelling concepts, which are not available in Event-B. In particular, UML-B includes class diagram and state machine diagram editors with ...
A generic framework: from modeling to code
Model-driven development (MDD) is a very popular technique in the area of software development, but this technique is criticized due to lack of a formal semantics. MDD is used for large-scale system development using semi-formal techniques like UML (...
Comments