{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,5,5]],"date-time":"2023-05-05T14:10:18Z","timestamp":1683295818101},"reference-count":22,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2005,12,1]],"date-time":"2005-12-01T00:00:00Z","timestamp":1133395200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2005,12]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Computer aided hardware\/software partitioning is one of the key challenges in hardware\/software co-design. This paper describes a new approach to hardware\/software partitioning for a synchronous communication model including multiple hardware devices. We transform the partitioning into a reachability problem of timed automata. By means of an optimal reachability algorithm, the optimal solution can be obtained with limited resources in hardware. To relax the initial condition of the partitioning for optimization, two algorithms are designed to explore the dependency relations among processes in the sequential specification. Moreover, we propose a scheduling algorithm to improve the synchronous communication efficiency further after partitioning stage. Some experiments are conducted with the model checker UPPAAL to show our approach is both effective and efficient.<\/jats:p>","DOI":"10.1007\/s00165-005-0072-y","type":"journal-article","created":{"date-parts":[[2005,11,17]],"date-time":"2005-11-17T18:22:00Z","timestamp":1132251720000},"page":"443-460","source":"Crossref","is-referenced-by-count":1,"title":["Exploring optimal solution to hardware\/software partitioning for synchronous model"],"prefix":"10.1145","volume":"17","author":[{"given":"Jifeng","family":"He","sequence":"first","affiliation":[{"name":"International Institute for Software Technology, United Nations University, Macau, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dang Van","family":"Hung","sequence":"additional","affiliation":[{"name":"International Institute for Software Technology, United Nations University, Macau, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Geguang","family":"Pu","sequence":"additional","affiliation":[{"name":"LMAM and Department of Informatics, School of Mathematics, Peking University, 100871, Beijing, China"},{"name":"Software Engineering Institute, East China Normal University, 200062, Shanghai, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zongyan","family":"Qiu","sequence":"additional","affiliation":[{"name":"LMAM and Department of Informatics, School of Mathematics, Peking University, 100871, Beijing, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Wang","family":"Yi","sequence":"additional","affiliation":[{"name":"Department of Computer Systems, Uppsala University, Uppsala, Sweden"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"issue":"2","key":"p_1","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","article-title":"A theory for timed automata","volume":"126","author":"Alur R","year":"1994","journal-title":"Theor Comput Sci"},{"key":"p_2","doi-asserted-by":"crossref","first-page":"709","DOI":"10.1109\/DAC.1997.597236","volume-title":"Proceedings of Design automation conference, ACM Press","author":"Agrawal S","year":"1997"},{"key":"p_3","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0304-3975(88)90051-5","article-title":"Theory of traces","volume":"60","author":"Aalbersberg IJ","year":"1988","journal-title":"Theor Comput Sci"},{"key":"p_4","first-page":"546","volume-title":"Proceedings of CAV'98 (LNCS 1427)","author":"Bozga M","year":"1998"},{"key":"p_5","first-page":"174","volume-title":"Proceedings of TACAS'01","author":"Behrmann G","year":"2001"},{"key":"p_6","doi-asserted-by":"crossref","first-page":"147","DOI":"10.1007\/3-540-45351-2_15","volume-title":"Proceedings of the 4th international workwhop on hybrid systems: computation and control (HSCC'01)","author":"Behrmann G","year":"2001"},{"issue":"1","key":"p_7","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1023\/A:1011184310224","article-title":"An approach to the specification and verification of a hardware compilation scheme","volume":"19","author":"Bowen J","year":"2001","journal-title":"J Supercomput"},{"key":"p_8","first-page":"220","volume-title":"Proceedings of EuroDAC","author":"Barros E","year":"1994"},{"key":"p_9","first-page":"197","volume-title":"Proceedings of automatic verification methods for finite state systems (LNCS 407)","author":"Dil DL","year":"1989"},{"key":"p_10","volume-title":"Singapore","author":"Diekert V","year":"1995"},{"key":"p_12","volume-title":"Unifying theories of programming","author":"Hoare CAR","year":"1998","edition":"1"},{"key":"p_13","doi-asserted-by":"crossref","first-page":"460","DOI":"10.1007\/3-540-63166-6_48","volume-title":"Proceedings of the 9th international conference on computer aided verification (LNCS 1254)","author":"Henzinger TA","year":"1997"},{"key":"p_15","first-page":"1400","volume-title":"World congress on formal methods 1999 (WCFM 99)","author":"Iyoda J","year":"1999"},{"key":"p_16","doi-asserted-by":"crossref","first-page":"62","DOI":"10.1007\/3-540-60249-6_41","volume-title":"Proceedings of the 10th international conference on fundamentals of computation theory (LNCS 965)","author":"Larsen KG","year":"1995"},{"issue":"2","key":"p_17","doi-asserted-by":"crossref","first-page":"134","DOI":"10.1007\/s100090050010","article-title":"UPPAAL in a nutshell","volume":"1","author":"Larsen KG","year":"1997","journal-title":"Softw Tools Technol Transf"},{"key":"p_18","volume-title":"The Occam 2 Programming Manual","author":"Ltd INMOS","year":"1988"},{"issue":"2","key":"p_19","doi-asserted-by":"crossref","first-page":"165","DOI":"10.1023\/A:1008832202436","article-title":"An algorithm for hardware\/software partitioning using mixed integer linear programming","volume":"2","author":"Nieman R","year":"1997","journal-title":"Des Automat Embedded Syst"},{"key":"p_21","first-page":"316","volume-title":"IEEE\/ACM Proceedings of the european conference on design automation (EuroDAC), ACM Press","author":"Peng Z","year":"1993"},{"key":"p_23","first-page":"273","volume-title":"Proceedings of the 7th IEEE international conference on electronics, circuits and systems, IEEE","author":"Qin S","year":"2000"},{"key":"p_24","first-page":"652","volume-title":"Internatitional conference on computer design, IEEE","author":"Quan G","year":"1999"},{"key":"p_25","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4757-2649-7","volume-title":"Hardware\/software co-design: principles and practice","author":"Staunstrup J","year":"1997"},{"key":"p_26","first-page":"227","volume-title":"LNCS 975","author":"Wei M","year":"1997"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-005-0072-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-005-0072-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-005-0072-y","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,5]],"date-time":"2023-05-05T13:40:28Z","timestamp":1683294028000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-005-0072-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005,12]]},"references-count":22,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2005,12]]}},"alternative-id":["10.1007\/s00165-005-0072-y"],"URL":"https:\/\/doi.org\/10.1007\/s00165-005-0072-y","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2005,12]]}}}