{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:31:27Z","timestamp":1750307487108,"version":"3.41.0"},"reference-count":45,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2012,1,27]],"date-time":"2012-01-27T00:00:00Z","timestamp":1327622400000},"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":[[2012,1,27]]},"abstract":"<jats:p>Capacity limitations continue to impede widespread adoption of formal property verification in the design validation ow of software and hardware systems. The more popular choice (at least in the hardware domain) has been dynamic property verification (DPV), which is a semi-formal approach where the formal properties are checked over simulation runs. DPV is highly scalable and can support a rich specification language. The main contribution of this paper is to build an integrated DPV platform for validation of UML-based designs. Specifically, we present (a) a language, named Action-LTL (a simple extension of Linear Temporal Logic) for writing assertions over data attributes and events of UML models, and (b) an integrated dynamic assertion-verification platform for verification of UML designs. In view of the capacity limitations of existing formal property verification tools, we believe that the methods presented in this paper are of immediate practical value to the UML design community.<\/jats:p>","DOI":"10.1145\/2088883.2088891","type":"journal-article","created":{"date-parts":[[2012,2,14]],"date-time":"2012-02-14T13:21:07Z","timestamp":1329225667000},"page":"1-14","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["A dynamic assertion-based verification platform for validation of UML designs"],"prefix":"10.1145","volume":"37","author":[{"given":"A.","family":"Banerjee","sequence":"first","affiliation":[{"name":"Advanced Computing and Microelectronics Unit, Indian Statistical Institute"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"S.","family":"Ray","sequence":"additional","affiliation":[{"name":"Dept. of Computer Science &amp; Engineering, IIT Kharagpur"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"P.","family":"Dasgupta","sequence":"additional","affiliation":[{"name":"Dept. of Computer Science &amp; Engineering, IIT Kharagpur"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"P. P.","family":"Chakrabarti","sequence":"additional","affiliation":[{"name":"Dept. of Computer Science &amp; Engineering, IIT Kharagpur"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"S.","family":"Ramesh","sequence":"additional","affiliation":[{"name":"General Motors India Science Lab"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"P.","family":"Vignesh","sequence":"additional","affiliation":[{"name":"General Motors India Science Lab"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"V.","family":"Ganesan","sequence":"additional","affiliation":[{"name":"General Motors India Science Lab"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2012,1,27]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-88387-6_18"},{"volume-title":"IEEE TENCON 2008","author":"Banerjee A.","key":"e_1_2_1_2_1","unstructured":"Banerjee , A. , Ray , S. , Dasgupta , P. , Chakrabarti P. P. , Ramesh S. and Ganesan , P.V.V. , A Dynamic Assertion-based Verification Platform for UML Statecharts over Rhapsody , In IEEE TENCON 2008 Banerjee, A., Ray, S., Dasgupta, P., Chakrabarti P. P., Ramesh S. and Ganesan, P.V.V., A Dynamic Assertion-based Verification Platform for UML Statecharts over Rhapsody, In IEEE TENCON 2008"},{"key":"e_1_2_1_3_1","volume-title":"Model Checking of Statechart Models: Survey and Recent Directions","author":"Bhaduri P.","year":"2004","unstructured":"Bhaduri , P. and Ramesh , S. , Model Checking of Statechart Models: Survey and Recent Directions , 2004 Bhaduri, P. and Ramesh, S., Model Checking of Statechart Models: Survey and Recent Directions, 2004"},{"key":"e_1_2_1_4_1","unstructured":"Bodden E. \"J-LO A tool for runtime-checking temporal assertions \" Diploma Thesis 2005.  Bodden E. \"J-LO A tool for runtime-checking temporal assertions \" Diploma Thesis 2005."},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.5555\/647544.730470"},{"key":"e_1_2_1_6_1","series-title":"LNCS","volume-title":"Fundamental Approaches to Software Engineering (FASE","author":"Bradfield J.","year":"2002","unstructured":"Bradfield , J. , Kuester , F. , and Stevens , P. , Enriching OCL Using Observational mu-calculus . In R.D. Kutsche and H. Weber, editors, Fundamental Approaches to Software Engineering (FASE 2002 ), Grenoble, France , volume 2306 of LNCS . Springer , April 2002. Bradfield, J., Kuester, F., and Stevens, P., Enriching OCL Using Observational mu-calculus. In R.D. Kutsche and H. Weber, editors, Fundamental Approaches to Software Engineering (FASE 2002), Grenoble, France, volume 2306 of LNCS. Springer, April 2002."},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1016\/B978-044482830-9\/50022-9"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.5555\/647541.730162"},{"key":"e_1_2_1_10_1","volume-title":"Formal Aspects of Computing 17(4)","author":"Chaki S.","year":"2005","unstructured":"Chaki , S. , Clarke , E. , Ouaknine , J. , Sharygina , N. , and Sinha , N. , Concurrent software verification with states, events, and deadlocks , Formal Aspects of Computing 17(4) , 2005 . Chaki, S., Clarke, E., Ouaknine, J., Sharygina, N., and Sinha, N., Concurrent software verification with states, events, and deadlocks, Formal Aspects of Computing 17(4), 2005."},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24756-2_8"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1297027.1297069"},{"key":"e_1_2_1_13_1","volume-title":"Model Checking","author":"Clarke E.M.","year":"2000","unstructured":"Clarke , E.M. , Grumberg , O. , and Peled , D.A. , Model Checking , MIT Press , 2000 . Clarke, E.M., Grumberg, O., and Peled, D.A., Model Checking, MIT Press, 2000."},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1083246.1083249"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1011227529550"},{"key":"e_1_2_1_16_1","volume-title":"A Roadmap for Formal Property Verification","author":"Dasgupta P.","year":"2006","unstructured":"Dasgupta , P. , A Roadmap for Formal Property Verification , Springer 2006 . Dasgupta, P., A Roadmap for Formal Property Verification, Springer 2006."},{"key":"e_1_2_1_17_1","series-title":"LNCS","first-page":"389","volume-title":"Object modeling with the OCL: The Rationale behind the Object Constraint Language","author":"Flake S.","year":"2002","unstructured":"Flake , S. , and Mueller , W. , An OCL Extension for Real-Time Constraints . In Object modeling with the OCL: The Rationale behind the Object Constraint Language , volume 2263 of LNCS , pages 389 -- 408 , Springer , 2002 . Flake, S., and Mueller, W., An OCL Extension for Real-Time Constraints. In Object modeling with the OCL: The Rationale behind the Object Constraint Language, volume 2263 of LNCS, pages 389--408, Springer, 2002."},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/940071.940106"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/940071.940078"},{"key":"e_1_2_1_20_1","first-page":"325","volume-title":"On the Executable Core of the UML), LNCS","author":"Harel D.","year":"2004","unstructured":"Harel , D. and Kugler , H. , The Rhapsody semantics of Statecharts (or , On the Executable Core of the UML), LNCS vol. 3147 , Springer-Verlag , pages 325 -- 354 , 2004 . Harel, D. and Kugler, H., The Rhapsody semantics of Statecharts (or, On the Executable Core of the UML), LNCS vol. 3147, Springer-Verlag, pages 325--354, 2004."},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.5555\/645395.651926"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.5555\/647745.734059"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(82)90125-6"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/s001659970003"},{"key":"e_1_2_1_25_1","volume-title":"IEEE Computer Society","author":"Lilius J.","year":"1999","unstructured":"Lilius , J. , and Porres , I ., vUML: a tool for In Proceedings of the Automatic Software Engineering Conference (ASE) , IEEE Computer Society , 1999 . Lilius, J., and Porres, I., vUML: a tool for In Proceedings of the Automatic Software Engineering Conference (ASE), IEEE Computer Society, 1999."},{"key":"e_1_2_1_26_1","unstructured":"LTSA website. http:\/\/www-dse.doc.ic.ac.uk\/concurrency\/ltsa\/LTSA.html  LTSA website. http:\/\/www-dse.doc.ic.ac.uk\/concurrency\/ltsa\/LTSA.html"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/201019.201032"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1016\/0169-7552(93)90047-8"},{"key":"e_1_2_1_29_1","volume-title":"Workshop SVERTS on Specification and Validation of UML models for Real Time and Embedded Systems, a satellite event of UML 2003","author":"Ober I.","year":"2003","unstructured":"Ober , I. , Graf , S. , and Ober , I ., Validating timed UML models by simulation and verification . In Workshop SVERTS on Specification and Validation of UML models for Real Time and Embedded Systems, a satellite event of UML 2003 , San Francisco , October 2003 . Ober, I., Graf, S., and Ober, I., Validating timed UML models by simulation and verification. In Workshop SVERTS on Specification and Validation of UML models for Real Time and Embedded Systems, a satellite event of UML 2003, San Francisco, October 2003."},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24732-6_9"},{"key":"e_1_2_1_31_1","volume-title":"Version 1.4","author":"Object Management Group","year":"2001","unstructured":"Object Management Group , Unified Modeling Language Specification , Version 1.4 , Draft , OMG( 2001 ), http:\/\/cgi.omg.org\/cgibin\/docad\/018214. Object Management Group, Unified Modeling Language Specification, Version 1.4, Draft, OMG(2001), http:\/\/cgi.omg.org\/cgibin\/docad\/018214."},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1977.32"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.5555\/19518.19527"},{"key":"e_1_2_1_34_1","unstructured":"Schinz I. Toben T. Mrugulla C. and Westphal B. The Rhapsody UML Verification Environment  Schinz I. Toben T. Mrugulla C. and Westphal B. The Rhapsody UML Verification Environment"},{"volume-title":"Electronic Notes in Theoretical Computer Science","author":"Sch\u00e4fer T.","key":"e_1_2_1_35_1","unstructured":"Sch\u00e4fer , T. , Knapp , A. , and Merz , S. , Model checking UML state machines and collaborations . In Scott D. Stoller and Willem Visser, editors, Electronic Notes in Theoretical Computer Science , volume 55(3), Elsevier, 2001 . Sch\u00e4fer, T., Knapp, A., and Merz, S., Model checking UML state machines and collaborations. In Scott D. Stoller and Willem Visser, editors, Electronic Notes in Theoretical Computer Science, volume 55(3), Elsevier, 2001."},{"key":"e_1_2_1_36_1","volume-title":"Real-Time Object-Oriented Modeling","author":"Selic B.","year":"1994","unstructured":"Selic , B. , Gullekson , G. , and Ward , P. , Real-Time Object-Oriented Modeling . John Wiley & Sons, Inc. , 1994 . Selic, B., Gullekson, G., and Ward, P., Real-Time Object-Oriented Modeling. John Wiley & Sons, Inc., 1994."},{"key":"e_1_2_1_37_1","volume-title":"ObjectTime Limited","author":"Selic B.","year":"1998","unstructured":"Selic , B. , Rumbaugh , J. , Using UML for modeling complex real-time systems. Techreport , ObjectTime Limited , 1998 . Selic, B., Rumbaugh, J., Using UML for modeling complex real-time systems. Techreport, ObjectTime Limited, 1998."},{"key":"e_1_2_1_38_1","volume-title":"Proc. 16th IEEE International Conference on Automated Software Engineering (ASE 2001)","author":"Shen W.","year":"2001","unstructured":"Shen , W. , Compton , K. , and Huggins , J.K ., A toolset for supporting UML static and dynamic model checking . In Proc. 16th IEEE International Conference on Automated Software Engineering (ASE 2001) , 26-29 November 2001 , Coronado Island, San Diego, CA, USA, pages 315--318. IEEE Computer Society , 2001. Shen, W., Compton, K., and Huggins, J.K., A toolset for supporting UML static and dynamic model checking. In Proc. 16th IEEE International Conference on Automated Software Engineering (ASE 2001), 26-29 November 2001, Coronado Island, San Diego, CA, USA, pages 315--318. IEEE Computer Society, 2001."},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.5555\/647769.734097"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2006.02.007"},{"volume-title":"Primer and Reference Manual","author":"The Spin Model Checker","key":"e_1_2_1_41_1","unstructured":"The Spin Model Checker : Primer and Reference Manual , Addison-Wesley , ISBN 0-321-22862-6. The Spin Model Checker: Primer and Reference Manual, Addison-Wesley, ISBN 0-321-22862-6."},{"key":"e_1_2_1_42_1","unstructured":"The Local Interconnect Network Protocol http:\/\/www.lin-subbus.org\/  The Local Interconnect Network Protocol http:\/\/www.lin-subbus.org\/"},{"volume-title":"Primer and Reference Manual","author":"The Spin Model Checker","key":"e_1_2_1_43_1","unstructured":"The Spin Model Checker : Primer and Reference Manual , Addison-Wesley , ISBN 0-321-22862-6. The Spin Model Checker: Primer and Reference Manual, Addison-Wesley, ISBN 0-321-22862-6."},{"key":"e_1_2_1_44_1","volume-title":"Carnegie Mellon University","author":"Trace","year":"1988","unstructured":"Trace theory for automatic hierarchical verification of speed-independent circuits. PhD thesis , Carnegie Mellon University , 1988 . Technical report no. CMU-CS-88-119. Trace theory for automatic hierarchical verification of speed-independent circuits. PhD thesis, Carnegie Mellon University, 1988. Technical report no. CMU-CS-88-119."},{"key":"e_1_2_1_45_1","first-page":"428","volume-title":"the Proceedings of the 8th International Conference on Computer Aided Verification","author":"VIS","year":"1996","unstructured":"VIS : A system for Verification and Synthesis, The VIS Group , In the Proceedings of the 8th International Conference on Computer Aided Verification , p 428 -- 432 , Springer Lecture Notes in Computer Science, 1102, Edited by R. Alur and T. Henzinger, New Brunswick, NJ , July 1996 . VIS: A system for Verification and Synthesis, The VIS Group, In the Proceedings of the 8th International Conference on Computer Aided Verification, p428--432, Springer Lecture Notes in Computer Science, 1102, Edited by R. Alur and T. Henzinger, New Brunswick, NJ, July 1996."},{"key":"e_1_2_1_46_1","volume-title":"Proceedings of ASE-2001: The 16th IEEE Conference on Automated Software Engineering. IEEE CS Press","author":"Xie F.","year":"2001","unstructured":"Xie , F. , Levin , V. , and Browne , J.C ., Model Checking for an Executable Subset of UML. In M. Feather and M. Goedicke, editors , Proceedings of ASE-2001: The 16th IEEE Conference on Automated Software Engineering. IEEE CS Press , 2001 . Xie, F., Levin, V., and Browne, J.C., Model Checking for an Executable Subset of UML. In M. Feather and M. Goedicke, editors, Proceedings of ASE-2001: The 16th IEEE Conference on Automated Software Engineering. IEEE CS Press, 2001."}],"container-title":["ACM SIGSOFT Software Engineering Notes"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2088883.2088891","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2088883.2088891","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T12:09:13Z","timestamp":1750248553000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2088883.2088891"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,1,27]]},"references-count":45,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2012,1,27]]}},"alternative-id":["10.1145\/2088883.2088891"],"URL":"https:\/\/doi.org\/10.1145\/2088883.2088891","relation":{},"ISSN":["0163-5948"],"issn-type":[{"type":"print","value":"0163-5948"}],"subject":[],"published":{"date-parts":[[2012,1,27]]},"assertion":[{"value":"2012-01-27","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}