UML-B: Formal modeling and design aided by UML

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.

REFERENCES

• 1: J.-R. Abrial, The B-book: assigning programs to meanings, Cambridge University Press, New York, NY, 1996
• 2: 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.
• 3: B-Core 1996. B-Toolkit User's Manual, Release 3.2. B-Core(UK) Ltd., Oxford, UK.
• 4: Edmund M. Clarke, Jr. , Orna Grumberg , Doron A. Peled, Model checking, MIT Press, Cambridge, MA, 2000
• 5: Clearsy 2003. AtelierB User Manual V3.6. ClearSy System Engineering, Aix-en-Provence, F.
• 6: Clearsy 2000. AtelierB Training Course Level 2. ClearSy System Engineering, Aix-en-Provence, F.
• 7: Dan Craigen , Susan Gerhart , Ted Ralston, Formal Methods Reality Check: Industrial Usage, IEEE Transactions on Software Engineering, v.21 n.2, p.90-98, February 1995 [doi>10.1109/32.345825]
• 8: 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.
• 9: 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.
• 10: Robert L. Glass, The mystery of formal methods disuse, Communications of the ACM, v.47 n.8, August 2004 [doi>10.1145/1012037.1012052]
• 11: David Harel, Statecharts: A visual formalism for complex systems, Science of Computer Programming, v.8 n.3, p.231-274, June 1, 1987 [doi>10.1016/0167-6423(87)90035-9]
• 12: 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.
• 13: 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.
• 14: 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.
• 15: 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/
• 16: Mermet, J. (Ed.) 2004. UML-B Specification for Proven Embedded Systems Design. Kluwer Academic Publishers, Dordrecht, The Netherlands.
• 17: Eric Meyer , Jeanine Souquières, A Systematic Approach to Transform OMT Diagrams to a B Specification, Proceedings of the Wold Congress on Formal Methods in the Development of Computing Systems-Volume I, p.875-895, September 20-24, 1999
• 18: Naïma Nagui-Raïss, A Formal Software Specification Tool Using the Entity-Relationship Model, Proceedings of the13th International Conference on the Entity-Relationship Approach, p.315-332, December 13-16, 1994
• 19: James Rumbaugh , Ivar Jacobson , Grady Booch, The Unified Modeling Language reference manual, Addison-Wesley Longman Ltd., Essex, UK, 1998
• 20: Emil Sekerinski, Graphical Design of Reactive Systems, Proceedings of the Second International B Conference on Recent Advances in the Development and Use of the B Method, p.182-197, April 22-24, 1998
• 21: 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.
• 22: 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.
• 23: 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.
• 24: 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.
• 25: J. M. Spivey, Understanding Z: a specification language and its formal semantics, Cambridge University Press, New York, NY, 1988
• 26: Toval, A., Requena, A., and Alemán, J. L. 2003. Emerging OCL Tools. Software and System Modeling (SoSyM), 2, 40, 248--261.
• 27: 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.
• 28: 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.
• 29: Jos Warmer , Anneke Kleppe, The Object Constraint Language: Getting Your Models Ready for MDA, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 2003

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.1 Requirements/Specifications

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.2 Design Tools and Techniques
      D.2.4 Software/Program Verification

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs

General Terms:
Design, Verification

Keywords:
Modeling, UML-B, refinement