{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,28]],"date-time":"2025-09-28T04:08:53Z","timestamp":1759032533098,"version":"3.41.0"},"reference-count":45,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2007,9,1]],"date-time":"2007-09-01T00:00:00Z","timestamp":1188604800000},"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":["ACM Trans. Des. Autom. Electron. Syst."],"published-print":{"date-parts":[[2007,9]]},"abstract":"<jats:p>With the advent of multiprocessor embedded platforms, application partitioning and mapping have gained primacy as a design step. The output of this design step is a multithreaded partitioned application where each thread is mapped to a processing element (processor or ASIC) in the multiprocessor platform. This partitioned application must be verified to be consistent with the native unpartitioned application. This verification task is called application (or task) partitioning verification.<\/jats:p>\n          <jats:p>\n            This work proposes a code-block-level\n            <jats:italic>containment-checking<\/jats:italic>\n            -based methodology for application partitioning verification. We use a UML-based code-block-level modeling language which is rich enough to model most designs. We formulate the application partitioning verification problem as a special case of the containment checking problem, which we call the\n            <jats:italic>complete containment checking problem<\/jats:italic>\n            . We propose a state space reduction technique specific to the containment checking, reachability analysis, and deadlock detection problems. We propose novel data structures and token propagation methodologies which enhance the efficiency of containment checking. We present an efficient containment checking algorithm for the application partitioning verification problem. We develop a containment checking tool called TraceMatch and present experimental results. We present a comparison of the state space reduction achieved by TraceMatch with that achieved by formal analysis and verification tools like Spin, PEP, PROD, and LoLA.\n          <\/jats:p>","DOI":"10.1145\/1278349.1278357","type":"journal-article","created":{"date-parts":[[2007,10,14]],"date-time":"2007-10-14T12:41:11Z","timestamp":1192365671000},"page":"44","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":9,"title":["Functional verification of task partitioning for multiprocessor embedded systems"],"prefix":"10.1145","volume":"12","author":[{"given":"Dipankar","family":"Das","sequence":"first","affiliation":[{"name":"Indian Institute of Technology Kharagpur, Kharagpur, India"}]},{"given":"P. P.","family":"Chakrabarti","sequence":"additional","affiliation":[{"name":"Indian Institute of Technology Kharagpur, Kharagpur, India"}]},{"given":"Rajeev","family":"Kumar","sequence":"additional","affiliation":[{"name":"Indian Institute of Technology Kharagpur, Kharagpur, India"}]}],"member":"320","published-online":{"date-parts":[[2007,9]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"Mocha: Modularity in model checking. In Proceedings of the International Conference on Computer-Aided Verification (CAV), A. J. Hu and M","author":"Alur R.","year":"1998","unstructured":"Alur , R. , Henzinger , T.A. , Mang , F.Y.C. , Qadeer , S. , Rajamani , S.K. , and Tasiran , S . 1998 . Mocha: Modularity in model checking. In Proceedings of the International Conference on Computer-Aided Verification (CAV), A. J. Hu and M . Y. Vardi, eds. Lecture Notes in Computer Science, vol. 1427 . Springer , 521--525. Alur, R., Henzinger, T.A., Mang, F.Y.C., Qadeer, S., Rajamani, S.K., and Tasiran, S. 1998. Mocha: Modularity in model checking. In Proceedings of the International Conference on Computer-Aided Verification (CAV), A. J. Hu and M. Y. Vardi, eds. Lecture Notes in Computer Science, vol. 1427. Springer, 521--525."},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/2.982917"},{"volume-title":"the FEmSys Conference. Tool presentation.","author":"Best E.","key":"e_1_2_1_3_1","unstructured":"Best , E. , Esparza , J. , Grahlmann , B. , Melzer , S. , R\u00f6mer , S. , and Wallner , F . 1997. The PEP verification system . In the FEmSys Conference. Tool presentation. Best, E., Esparza, J., Grahlmann, B., Melzer, S., R\u00f6mer, S., and Wallner, F. 1997. The PEP verification system. In the FEmSys Conference. Tool presentation."},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/200836.200876"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/828.833"},{"key":"e_1_2_1_6_1","first-page":"155","article-title":"Ptolemy: A framework for simulating and prototyping heterogenous systems","volume":"4","author":"Buck J.","year":"1994","unstructured":"Buck , J. , Ha , S. , Lee , E.A. , and Messerschmitt , D.G. 1994 . Ptolemy: A framework for simulating and prototyping heterogenous systems . Int. J. Comput. Simul. 4 , 2, 155 -- 182 . Buck, J., Ha, S., Lee, E.A., and Messerschmitt, D.G. 1994. Ptolemy: A framework for simulating and prototyping heterogenous systems. Int. J. Comput. Simul. 4, 2, 155--182.","journal-title":"Int. J. Comput. Simul."},{"key":"e_1_2_1_7_1","doi-asserted-by":"crossref","unstructured":"Chen R. Sgroi M. Lavagno L. Martin G. Sangiovanni-Vincentelli A. and Rabaey J. 2003. UML and platform-based design. 107--126.   Chen R. Sgroi M. Lavagno L. Martin G. Sangiovanni-Vincentelli A. and Rabaey J. 2003. UML and platform-based design. 107--126.","DOI":"10.1007\/0-306-48738-1_5"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/151646.151648"},{"volume-title":"Proceedings of the IEEE International Conference on Computer-Aided Design (ICCAD), 126--129","author":"Coudert O.","key":"e_1_2_1_9_1","unstructured":"Coudert , O. and Madre , J.C . 1990. A unified framework for the formal verification of sequential circuits . In Proceedings of the IEEE International Conference on Computer-Aided Design (ICCAD), 126--129 . Coudert, O. and Madre, J.C. 1990. A unified framework for the formal verification of sequential circuits. In Proceedings of the IEEE International Conference on Computer-Aided Design (ICCAD), 126--129."},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/151257.151258"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040291.1040292"},{"key":"e_1_2_1_12_1","volume-title":"eds","author":"Edmund M.","year":"2001","unstructured":"Edmund , M. Clarke , J. , Grumberg , O. , and Peled , D. , eds . 2001 . Model Checking. MIT Press , Cambridge, MA. Edmund, M. Clarke, J., Grumberg, O., and Peled, D., eds. 2001. Model Checking. MIT Press, Cambridge, MA."},{"key":"e_1_2_1_13_1","doi-asserted-by":"crossref","unstructured":"Ellson J. Gansner E. Koutsofios E. North S. and Woodhull G. 2003. Graphviz and Dynagraph---Static and dynamic graph drawing tools. In Graph Drawing Software M. Junger and P. Mutzel eds. Springer 127--148.  Ellson J. Gansner E. Koutsofios E. North S. and Woodhull G. 2003. Graphviz and Dynagraph---Static and dynamic graph drawing tools. In Graph Drawing Software M. Junger and P. Mutzel eds. Springer 127--148.","DOI":"10.1007\/978-3-642-18638-7_6"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1125808.1125809"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2004.33"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1014746130920"},{"key":"e_1_2_1_17_1","unstructured":"Esparza J. Schr\u00f6ter C. and Schwoon S. 2006. The Model Checking Kit. http:\/\/www.fmi.uni-stuttgart.de\/szs\/tools\/mckit\/.University of Stuttgart.  Esparza J. Schr\u00f6ter C. and Schwoon S. 2006. The Model Checking Kit. http:\/\/www.fmi.uni-stuttgart.de\/szs\/tools\/mckit\/.University of Stuttgart."},{"key":"e_1_2_1_18_1","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"Finkbeiner B.","unstructured":"Finkbeiner , B. 2001. Language containment checking with nondeterministic BDDs . In Proceedings of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS) . Lecture Notes in Computer Science , vol. 2031 . Springer , 24--38. Finkbeiner, B. 2001. Language containment checking with nondeterministic BDDs. In Proceedings of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Lecture Notes in Computer Science, vol. 2031. Springer, 24--38."},{"volume-title":"Papers from the 12th International Conference on Applications and Theory of Petri Nets (London)","author":"Finkel A.","key":"e_1_2_1_19_1","unstructured":"Finkel , A. 1993. The minimal coverability graph for Petri nets . In Papers from the 12th International Conference on Applications and Theory of Petri Nets (London) . Springer , 210--243. Finkel, A. 1993. The minimal coverability graph for Petri nets. In Papers from the 12th International Conference on Applications and Theory of Petri Nets (London). Springer, 210--243."},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.5555\/1128020.1128563"},{"key":"e_1_2_1_21_1","doi-asserted-by":"crossref","unstructured":"Haugen O. Muller-Pedersen B. and Weigert T. 2003. Structural modeling with UML 2.0: Classes interactions and state machines. 53--76.   Haugen O. Muller-Pedersen B. and Weigert T. 2003. Structural modeling with UML 2.0: Classes interactions and state machines. 53--76.","DOI":"10.1007\/0-306-48738-1_3"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2455.2460"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.588521"},{"key":"e_1_2_1_24_1","doi-asserted-by":"crossref","unstructured":"Hopcroft J.E. Motwani R. and Ullman J.D. 2000. Introduction to Automata Theory Languages and Computation 2nd ed. Addison Wesley.   Hopcroft J.E. Motwani R. and Ullman J.D. 2000. Introduction to Automata Theory Languages and Computation 2nd ed. Addison Wesley.","DOI":"10.1145\/568438.568455"},{"key":"e_1_2_1_25_1","unstructured":"Intel. 2006. Intel PRO\/Wireless 5116 broadband interface.  Intel. 2006. Intel PRO\/Wireless 5116 broadband interface."},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/107004.107032"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/293677.293681"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/277044.277060"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/307988.307989"},{"volume-title":"1980. On the Construction of Programs","author":"McKeag R.M.","key":"e_1_2_1_30_1","unstructured":"McKeag , R.M. and MacNaughten , A.M. , eds. 1980. On the Construction of Programs . Cambridge University Press , New York . McKeag, R.M. and MacNaughten, A.M., eds. 1980. On the Construction of Programs. Cambridge University Press, New York."},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1109\/MSPEC.2006.1572345"},{"volume-title":"Principles of Artificial Intelligence. Morgan Kaufmann","author":"Nilsson N.J.","key":"e_1_2_1_32_1","unstructured":"Nilsson , N.J. 1980. Principles of Artificial Intelligence. Morgan Kaufmann , San Francisco, CA . Nilsson, N.J. 1980. Principles of Artificial Intelligence. Morgan Kaufmann, San Francisco, CA."},{"key":"e_1_2_1_33_1","unstructured":"OMG. 2006. UML resource page. http:\/\/www.uml.org\/#Links-UML2Tools.  OMG. 2006. UML resource page. http:\/\/www.uml.org\/#Links-UML2Tools."},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00121262"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/356698.356702"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(78)90036-1"},{"key":"e_1_2_1_38_1","first-page":"2","article-title":"Distributed verification with Lola","volume":"54","author":"Schmidt K.","year":"2003","unstructured":"Schmidt , K. 2003 . Distributed verification with Lola . Fundam. Inf. 54 , 2 - 3 , 253--262. Schmidt, K. 2003. Distributed verification with Lola. Fundam. Inf. 54, 2-3, 253--262.","journal-title":"Fundam. Inf."},{"key":"e_1_2_1_39_1","doi-asserted-by":"crossref","unstructured":"Selic B. and Rumbaugh J. 1998. Using UML for modeling complex real-time systems. Tech. Rep. ObjecTime Limited.  Selic B. and Rumbaugh J. 1998. Using UML for modeling complex real-time systems. Tech. Rep. ObjecTime Limited.","DOI":"10.1007\/BFb0057795"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/800125.804029"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1109\/VLHCC.2004.46"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICVD.2005.155"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.5555\/111948.111969"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/233551.233556"},{"key":"e_1_2_1_45_1","volume-title":"Proceedings of the 9th International Conference on Computer Aided Verification (CAV)","volume":"1254","author":"Varpaaniemi K.","unstructured":"Varpaaniemi , K. , Heljanko , K. , and Lilius , J . 1997. PROD 3.2---An advanced tool for efficient reachability analysis . In Proceedings of the 9th International Conference on Computer Aided Verification (CAV) , Haifa, Israel, Jun. 22--25), O. Grumberg, ed. Lecture Notes in Computer Science , vol. 1254 . Springer, 472--475. Varpaaniemi, K., Heljanko, K., and Lilius, J. 1997. PROD 3.2---An advanced tool for efficient reachability analysis. In Proceedings of the 9th International Conference on Computer Aided Verification (CAV), Haifa, Israel, Jun. 22--25), O. Grumberg, ed. Lecture Notes in Computer Science, vol. 1254. Springer, 472--475."},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/267580.267590"}],"container-title":["ACM Transactions on Design Automation of Electronic Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1278349.1278357","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1278349.1278357","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T14:47:29Z","timestamp":1750258049000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1278349.1278357"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,9]]},"references-count":45,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2007,9]]}},"alternative-id":["10.1145\/1278349.1278357"],"URL":"https:\/\/doi.org\/10.1145\/1278349.1278357","relation":{},"ISSN":["1084-4309","1557-7309"],"issn-type":[{"type":"print","value":"1084-4309"},{"type":"electronic","value":"1557-7309"}],"subject":[],"published":{"date-parts":[[2007,9]]},"assertion":[{"value":"2007-09-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}