{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,16]],"date-time":"2025-10-16T03:49:18Z","timestamp":1760586558836,"version":"3.41.0"},"reference-count":26,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2011,1,24]],"date-time":"2011-01-24T00:00:00Z","timestamp":1295827200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["SIGSOFT Softw. Eng. Notes"],"published-print":{"date-parts":[[2011,1,24]]},"abstract":"<jats:p>In spite of its informal semantics and of some ambiguities, UML is a widespread modelling language used in both industry and academia. On the other hand, Petri nets are a mathematical modelling language with a formal semantics and are well suited for formal verification. However, altough there is a growing interest in model checking techniques from industry, the software engineers continue to be unfamiliar with such a formalism. For that reason, it is convenient to supply formal verification techniques of UML diagrams that are completely automatic and transparent to the designer. This is the issue discussed in this paper. We propose to translate UML state diagrams into Coloured Petri nets on which verification of some desired properties can be checked automatically. We show on our example that, when expected properties are not checked, this is an opportunity to revise the model into a more adequate one<\/jats:p>","DOI":"10.1145\/1921532.1921561","type":"journal-article","created":{"date-parts":[[2011,3,17]],"date-time":"2011-03-17T12:40:16Z","timestamp":1300365616000},"page":"1-8","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":32,"title":["Formal verification of UML state diagrams"],"prefix":"10.1145","volume":"36","author":[{"given":"Christine","family":"Choppy","sequence":"first","affiliation":[{"name":"LIPN, CNRS UMR 7030, Universit\u00e9 Paris 13, Villetaneuse, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kais","family":"Klai","sequence":"additional","affiliation":[{"name":"LIPN, CNRS UMR 7030, Universit\u00e9 Paris 13, Villetaneuse, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hacene","family":"Zidani","sequence":"additional","affiliation":[{"name":"LIPN, CNRS UMR 7030, Universit\u00e9 Paris 13, Villetaneuse, France"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2011,1,24]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-04558-9","volume-title":"Systems and software verification: model-checking techniques and tools","author":"B\u00e9rard B.","year":"2001","unstructured":"B. B\u00e9rard , M. Bidoit , A. Finkel , F. Laroussinie , A. Petit , L. Petrucci , and Ph. Schnoebelen . Systems and software verification: model-checking techniques and tools . Springer-Verlag , 2001 . B. B\u00e9rard, M. Bidoit, A. Finkel, F. Laroussinie, A. Petit, L. Petrucci, and Ph. Schnoebelen. Systems and software verification: model-checking techniques and tools. Springer-Verlag, 2001."},{"issue":"5","key":"e_1_2_1_2_1","first-page":"265","article-title":"Dependability analysis in the early phases of UML -based system design","volume":"16","author":"Bondavalli Andrea","year":"2001","unstructured":"Andrea Bondavalli , Mario Dal Cin , Diego Latella , Istv\u00e1n Majzik , Andr\u00e1s Pataricza , and Giancarlo Savoia . Dependability analysis in the early phases of UML -based system design . Comput. Syst. Sci. Eng. , 16 ( 5 ): 265 -- 275 , 2001 . Andrea Bondavalli, Mario Dal Cin, Diego Latella, Istv\u00e1n Majzik, Andr\u00e1s Pataricza, and Giancarlo Savoia. Dependability analysis in the early phases of UML -based system design. Comput. Syst. Sci. Eng., 16(5):265--275, 2001.","journal-title":"Comput. Syst. Sci. Eng."},{"key":"e_1_2_1_3_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"276","DOI":"10.1007\/3-540-45397-0_9","volume-title":"Concurrent Object-Oriented Programming and Petri Nets","author":"Baresi Luciano","year":"2001","unstructured":"Luciano Baresi and Mauro Pezze . On formalizing UML with high-level Petri nets . In G. Agha, F. de Cindio, and G. Rozenberg, editors, Concurrent Object-Oriented Programming and Petri Nets , volume 2001 of Lecture Notes in Computer Science , pages 276 -- 304 . Springer , 2001 . Luciano Baresi and Mauro Pezze. On formalizing UML with high-level Petri nets. In G. Agha, F. de Cindio, and G. Rozenberg, editors, Concurrent Object-Oriented Programming and Petri Nets, volume 2001 of Lecture Notes in Computer Science, pages 276--304. Springer, 2001."},{"key":"e_1_2_1_4_1","first-page":"150","volume-title":"SEKE","author":"Dong Zhijiang","year":"2003","unstructured":"Zhijiang Dong , Yujian Fu , and Xudong He . Deriving hierarchical predicate\/transition nets from statechart diagrams . In SEKE , pages 150 -- 157 , 2003 . Zhijiang Dong, Yujian Fu, and Xudong He. Deriving hierarchical predicate\/transition nets from statechart diagrams. In SEKE, pages 150--157, 2003."},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.5555\/646847"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/4904.4999"},{"key":"e_1_2_1_7_1","unstructured":"GraphViz: http:\/\/www.graphviz.org\/.  GraphViz: http:\/\/www.graphviz.org\/."},{"key":"e_1_2_1_8_1","first-page":"213","volume-title":"SEKE","author":"Hu Z.","year":"2004","unstructured":"Z. Hu and S. M. Shatz . Mapping UML diagrams to a Petri net notation for system simulation . In SEKE , pages 213 -- 219 , 2004 . Z. Hu and S. M. Shatz. Mapping UML diagrams to a Petri net notation for system simulation. In SEKE, pages 213--219, 2004."},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSMC.1995.538189"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1109\/ISORC.2006.55"},{"key":"e_1_2_1_11_1","volume-title":"Coloured Petri Nets, Modelling and Validation of Concurrent Systems","author":"Jensen Kurt","year":"2008","unstructured":"Kurt Jensen and Lars M. Kristensen . Coloured Petri Nets, Modelling and Validation of Concurrent Systems . Springer Verlag Monograph , 2008 . Kurt Jensen and Lars M. Kristensen. Coloured Petri Nets, Modelling and Validation of Concurrent Systems. Springer Verlag Monograph, 2008."},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.5555\/2794608.3220933"},{"key":"e_1_2_1_13_1","first-page":"395","volume-title":"Damm and Olderog {DO02}","author":"Knapp Alexander","unstructured":"Alexander Knapp , Stephan Merz , and Christopher Rauh . Model checking - timed UML state machines and collaborations . In Damm and Olderog {DO02} , pages 395 -- 416 . Alexander Knapp, Stephan Merz, and Christopher Rauh. Model checking - timed UML state machines and collaborations. In Damm and Olderog {DO02}, pages 395--416."},{"key":"e_1_2_1_14_1","first-page":"395","volume-title":"Damm and Olderog {DO02}","author":"Knapp Alexander","unstructured":"Alexander Knapp , Stephan Merz , and Christopher Rauh . Model checking - timed UML state machines and collaborations . In Damm and Olderog {DO02} , pages 395 -- 416 . Alexander Knapp, Stephan Merz, and Christopher Rauh. Model checking - timed UML state machines and collaborations. In Damm and Olderog {DO02}, pages 395--416."},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12566-9_10"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11219-007-9020-9"},{"key":"e_1_2_1_17_1","unstructured":"LIP6\/MoVe. The CPN-AMI home page http:\/\/www.lip6.fr\/cpn-ami\/.  LIP6\/MoVe. The CPN-AMI home page http:\/\/www.lip6.fr\/cpn-ami\/."},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.5555\/519308.786917"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.5555\/128869"},{"key":"e_1_2_1_20_1","volume-title":"In 11th International SPIN Workshop on Model Checking of Software, 2004","volume":"2989","author":"Ober Iulian","year":"2004","unstructured":"Iulian Ober , Susanne Graf , and Ileana Ober . Model checking of UML models via a mapping to communicating extended timed automata . In In 11th International SPIN Workshop on Model Checking of Software, 2004 , volume 2989 of LNCS, 2004 . Iulian Ober, Susanne Graf, and Ileana Ober. Model checking of UML models via a mapping to communicating extended timed automata. In In 11th International SPIN Workshop on Model Checking of Software, 2004, volume 2989 of LNCS, 2004."},{"key":"e_1_2_1_21_1","unstructured":"Papyrus UML : http:\/\/www.papyrusuml.org\/.  Papyrus UML : http:\/\/www.papyrusuml.org\/."},{"key":"e_1_2_1_22_1","first-page":"295","volume-title":"Proc. of UMLn2000 Workshop - Dynamic Behaviour in UML Models: Semantic Questions","volume":"1939","author":"Pettit Robert G.","year":"2000","unstructured":"Robert G. Pettit , IV , Robert G. Pettit Iv , and Hassan Gomaa . Validation of dynamic behavior in UML using colored Petri nets . In Proc. of UMLn2000 Workshop - Dynamic Behaviour in UML Models: Semantic Questions , volume 1939 in LNCS, pages 295 -- 302 . Springer Verlag , 2000 . Robert G. Pettit, IV, Robert G. Pettit Iv, and Hassan Gomaa. Validation of dynamic behavior in UML using colored Petri nets. In Proc. of UMLn2000 Workshop - Dynamic Behaviour in UML Models: Semantic Questions, volume 1939 in LNCS, pages 295--302. Springer Verlag, 2000."},{"key":"e_1_2_1_23_1","doi-asserted-by":"crossref","unstructured":"Ivan\n      Paltor\n     and \n      Johan\n      Lilius\n    .\n  Formalising UML state machines for model checking\n  . In Robert B. France and Bernhard Rumpe editors UML volume \n  1723\n   of \n  Lecture Notes in Computer Science pages \n  430\n  --\n  445\n  . \n  Springer 1999\n  .   Ivan Paltor and Johan Lilius. Formalising UML state machines for model checking. In Robert B. France and Bernhard Rumpe editors UML volume 1723 of Lecture Notes in Computer Science pages 430--445. Springer 1999.","DOI":"10.1007\/3-540-46852-8_31"},{"key":"e_1_2_1_24_1","unstructured":"UML Revision Task Force. OMG UML Specification. http:\/\/www.uml.org.  UML Revision Task Force. OMG UML Specification. http:\/\/www.uml.org."},{"key":"e_1_2_1_25_1","volume-title":"PROD reference manual. Technical report b13","author":"Varpaaniemi K.","year":"1995","unstructured":"K. Varpaaniemi , K. Hiekkanen J. Halme , and T. Pyssysalo . PROD reference manual. Technical report b13 , Helsinki University of Technology , Digital Systems Laboratory. Espoo, Finland, 1995 . K. Varpaaniemi, K. Hiekkanen J. Halme, and T. Pyssysalo. PROD reference manual. Technical report b13, Helsinki University of Technology, Digital Systems Laboratory. Espoo, Finland, 1995."},{"key":"e_1_2_1_26_1","unstructured":"XSLT\n  : http:\/\/www.w3.org\/TR\/1999\/REC-xslt-19991116.  XSLT: http:\/\/www.w3.org\/TR\/1999\/REC-xslt-19991116."}],"container-title":["ACM SIGSOFT Software Engineering Notes"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1921532.1921561","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1921532.1921561","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T12:08:41Z","timestamp":1750248521000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1921532.1921561"}},"subtitle":["a petri net based approach"],"short-title":[],"issued":{"date-parts":[[2011,1,24]]},"references-count":26,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2011,1,24]]}},"alternative-id":["10.1145\/1921532.1921561"],"URL":"https:\/\/doi.org\/10.1145\/1921532.1921561","relation":{},"ISSN":["0163-5948"],"issn-type":[{"type":"print","value":"0163-5948"}],"subject":[],"published":{"date-parts":[[2011,1,24]]},"assertion":[{"value":"2011-01-24","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}