{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T00:30:59Z","timestamp":1725841859898},"reference-count":29,"publisher":"Association for Computing Machinery (ACM)","issue":"1","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Softw. Eng. Methodol."],"published-print":{"date-parts":[[2006,1]]},"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.<\/jats:p>","DOI":"10.1145\/1125808.1125811","type":"journal-article","created":{"date-parts":[[2006,5,8]],"date-time":"2006-05-08T16:09:20Z","timestamp":1147104560000},"page":"92-122","update-policy":"http:\/\/dx.doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":196,"title":["UML-B"],"prefix":"10.1145","volume":"15","author":[{"given":"Colin","family":"Snook","sequence":"first","affiliation":[{"name":"University of Southampton, UK"}]},{"given":"Michael","family":"Butler","sequence":"additional","affiliation":[{"name":"University of Southampton, UK"}]}],"member":"320","published-online":{"date-parts":[[2006,1]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"The B Book---Assigning Programs to Meanings","author":"Abrial J. R.","unstructured":"Abrial , J. R. 1996. The B Book---Assigning Programs to Meanings . Cambridge University Press , NY .]] Abrial, J. R. 1996. The B Book---Assigning Programs to Meanings. Cambridge University Press, NY.]]"},{"key":"e_1_2_1_2_1","volume-title":"Practical Elements of Safety: Proceedings of the twelfth Safety-Critical Systems Symposium","author":"Amey P.","year":"2004","unstructured":"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.]] 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.]]"},{"key":"e_1_2_1_3_1","volume-title":"Release 3.2","author":"Core","unstructured":"B- Core 1996. B-Toolkit User's Manual , Release 3.2 . B-Core(UK) Ltd ., Oxford, UK.]] B-Core 1996. B-Toolkit User's Manual, Release 3.2. B-Core(UK) Ltd., Oxford, UK.]]"},{"key":"e_1_2_1_4_1","unstructured":"Clarke E. M. Grumberg O. and Peled D. 1999. Model Checking. MIT Press Cambridge MA.]] Clarke E. M. Grumberg O. and Peled D. 1999. Model Checking. MIT Press Cambridge MA.]]"},{"key":"e_1_2_1_5_1","unstructured":"Clearsy 2003. AtelierB User Manual V3.6. ClearSy System Engineering Aix-en-Provence F.]] Clearsy 2003. AtelierB User Manual V3.6. ClearSy System Engineering Aix-en-Provence F.]]"},{"key":"e_1_2_1_6_1","unstructured":"Clearsy 2000. AtelierB Training Course Level 2. ClearSy System Engineering Aix-en-Provence F.]] Clearsy 2000. AtelierB Training Course Level 2. ClearSy System Engineering Aix-en-Provence F.]]"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.345825"},{"key":"e_1_2_1_8_1","volume-title":"Methods Integration Workshop, Electronic Workshops in Computing (eWiC)","author":"Facon P.","unstructured":"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.]] 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.]]"},{"key":"e_1_2_1_9_1","unstructured":"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.]] 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.]]"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1012037.1012052"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(87)90035-9"},{"key":"e_1_2_1_12_1","volume-title":"4th International Conference, IFM 2004","author":"Lano K.","year":"2004","unstructured":"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.]] 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.]]"},{"key":"e_1_2_1_13_1","volume-title":"Informatik 2001 Workshop on Integrating Diagrammatic and Formal Specification Techniques","author":"Ledang H.","year":"2001","unstructured":"Ledang , H. and Souqui\u00e8res , 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.]] Ledang, H. and Souqui\u00e8res, 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.]]"},{"key":"e_1_2_1_14_1","volume-title":"Proceedings of Formal Methods Europe, FME","volume":"2805","author":"Leuschel M.","year":"2003","unstructured":"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.]] 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.]]"},{"key":"e_1_2_1_15_1","volume-title":"Methodologies and Technologies for Industrial Strength Systems Engineering (MATISSE) IST Programme RTD Research Project IST-1999-11435","author":"Matisse","year":"2000","unstructured":"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\/]] 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\/]]"},{"key":"e_1_2_1_16_1","volume-title":"2004. UML-B Specification for Proven Embedded Systems Design","author":"Mermet J.","unstructured":"Mermet , J. (Ed.) 2004. UML-B Specification for Proven Embedded Systems Design . Kluwer Academic Publishers , Dordrecht, The Netherlands.]] Mermet, J. (Ed.) 2004. UML-B Specification for Proven Embedded Systems Design. Kluwer Academic Publishers, Dordrecht, The Netherlands.]]"},{"key":"e_1_2_1_17_1","volume-title":"World Congress on Formal Methods in the Development of Computing Systems, FM'99","author":"Meyer E.","year":"1999","unstructured":"Meyer , E. and Souqui\u00e8res , 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.]] Meyer, E. and Souqui\u00e8res, 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.]]"},{"key":"e_1_2_1_18_1","volume-title":"13th International Conference on the Entity-Relationship Approach","volume":"881","author":"Nagui-Raiss N.","year":"1994","unstructured":"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.]] 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.]]"},{"key":"e_1_2_1_19_1","unstructured":"Rumbaugh J. Jacobson I. and Booch G. 1998. The Unified Modeling Language Reference Manual. Addison-Wesley Reading MA.]] Rumbaugh J. Jacobson I. and Booch G. 1998. The Unified Modeling Language Reference Manual. Addison-Wesley Reading MA.]]"},{"key":"e_1_2_1_20_1","volume-title":"B'98: Recent Advances in the Development and Use of the B Method---2nd International B Conference","volume":"1393","author":"Sekerinski E.","year":"1998","unstructured":"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.]] 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.]]"},{"key":"e_1_2_1_21_1","volume-title":"Proceedings of the 1st Conference on the B method","author":"Shore R.","year":"1996","unstructured":"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.]] 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.]]"},{"key":"e_1_2_1_22_1","doi-asserted-by":"crossref","unstructured":"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.]] 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.]]","DOI":"10.1007\/978-1-4020-2867-0_5"},{"key":"e_1_2_1_23_1","doi-asserted-by":"crossref","unstructured":"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.]] 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.]]","DOI":"10.1007\/978-1-4020-2867-0_6"},{"key":"e_1_2_1_24_1","volume-title":"Proceedings of RCS'2003 International Workshop on Refinement of Critical Systems: Methods, Tools and Experience","author":"Snook C.","unstructured":"Snook , C. , Tsiopoulos , L. , and Wald\u00e9n , 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.]] Snook, C., Tsiopoulos, L., and Wald\u00e9n, 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.]]"},{"key":"e_1_2_1_25_1","volume-title":"Understanding Z a specification language and its formal semantics","author":"Spivey J. M.","unstructured":"Spivey , J. M. 1988. Understanding Z a specification language and its formal semantics . Cambridge University Press , NY .]] Spivey, J. M. 1988. Understanding Z a specification language and its formal semantics. Cambridge University Press, NY.]]"},{"key":"e_1_2_1_26_1","doi-asserted-by":"crossref","first-page":"248","DOI":"10.1007\/s10270-003-0031-0","article-title":"Emerging OCL Tools","volume":"2","author":"Toval A.","year":"2003","unstructured":"Toval , A. , Requena , A. , and Alem\u00e1n , J. L. 2003 . Emerging OCL Tools . Software and System Modeling (SoSyM) , 2 , 40, 248 -- 261 .]] Toval, A., Requena, A., and Alem\u00e1n, J. L. 2003. Emerging OCL Tools. Software and System Modeling (SoSyM), 2, 40, 248--261.]]","journal-title":"Software and System Modeling (SoSyM)"},{"key":"e_1_2_1_27_1","unstructured":"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.]] 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.]]"},{"key":"e_1_2_1_28_1","doi-asserted-by":"crossref","first-page":"67","DOI":"10.1007\/s10617-005-1184-6","article-title":"Embedded System Design Using Formal Model Refinement: An Approach Based on the Combined Use of UML and the B Language","volume":"9","author":"Voros N.","year":"2004","unstructured":"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 .]] 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.]]","journal-title":"Design Automation for Embedded Systems"},{"key":"e_1_2_1_29_1","unstructured":"Warmer J. and Kleppe A. 2003. The Object Constraint Language Second Edition: Getting your models ready for MDA. Addison-Wesley.]] Warmer J. and Kleppe A. 2003. The Object Constraint Language Second Edition: Getting your models ready for MDA. Addison-Wesley.]]"}],"container-title":["ACM Transactions on Software Engineering and Methodology"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1125808.1125811","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,12,28]],"date-time":"2022-12-28T21:14:16Z","timestamp":1672262056000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1125808.1125811"}},"subtitle":["Formal modeling and design aided by UML"],"short-title":[],"issued":{"date-parts":[[2006,1]]},"references-count":29,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2006,1]]}},"alternative-id":["10.1145\/1125808.1125811"],"URL":"https:\/\/doi.org\/10.1145\/1125808.1125811","relation":{},"ISSN":["1049-331X","1557-7392"],"issn-type":[{"value":"1049-331X","type":"print"},{"value":"1557-7392","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006,1]]},"assertion":[{"value":"2006-01-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}