{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,19]],"date-time":"2026-03-19T06:26:48Z","timestamp":1773901608016,"version":"3.50.1"},"reference-count":37,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2006,2,1]],"date-time":"2006-02-01T00:00:00Z","timestamp":1138752000000},"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. Embed. Comput. Syst."],"published-print":{"date-parts":[[2006,2]]},"abstract":"<jats:p>This paper addresses the interrelation between control and data flow in embedded system models through a new design representation, called Dual Flow Net (DFN). A modeling formalism with a very close-fitting control and data flow is achieved by this representation, as a consequence of enhancing its underlying Petri net structure. The work presented in this paper does not only tackle the modeling side in embedded systems design, but also the validation of embedded system models through formal methods. Various introductory examples illustrate the applicability of the DFN principles, whereas the capability of the model to with complex designs is demonstrated through the design and verification of a real-life Ethernet coprocessor.<\/jats:p>","DOI":"10.1145\/1132357.1132360","type":"journal-article","created":{"date-parts":[[2006,7,25]],"date-time":"2006-07-25T14:14:26Z","timestamp":1153836866000},"page":"54-81","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":12,"title":["Dual Flow Nets"],"prefix":"10.1145","volume":"5","author":[{"given":"Mauricio","family":"Varea","sequence":"first","affiliation":[{"name":"University of Southampton, Southampton, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bashir M.","family":"Al-Hashimi","sequence":"additional","affiliation":[{"name":"University of Southampton, Southampton, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Luis A.","family":"Cort\u00e9S","sequence":"additional","affiliation":[{"name":"Link\u00f6ping University, Link\u00f6ping, Sweden"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Petru","family":"Eles","sequence":"additional","affiliation":[{"name":"Link\u00f6ping University, Link\u00f6ping, Sweden"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zebo","family":"Peng","sequence":"additional","affiliation":[{"name":"Link\u00f6ping University, Link\u00f6ping, Sweden"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2006,2]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"Information Processing Systems---Local Area Networks---Part 3: Carrier Sense Multiple Access with colision Detection (CSMA\/CD) access method and physical Layer Specifications","unstructured":"ANSI\/IEEE. 1991. Information Processing Systems---Local Area Networks---Part 3: Carrier Sense Multiple Access with colision Detection (CSMA\/CD) access method and physical Layer Specifications . IEEE , New York . ANSI\/IEEE. 1991. Information Processing Systems---Local Area Networks---Part 3: Carrier Sense Multiple Access with colision Detection (CSMA\/CD) access method and physical Layer Specifications. IEEE, New York."},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/349194.349197"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(92)90017-A"},{"key":"e_1_2_1_5_1","unstructured":"Cadence. 2001. The SMV Model Checker. http:\/\/www-cad.eecs.berkeley.edu\/~kenmcmil\/smv\/.  Cadence. 2001. The SMV Model Checker. http:\/\/www-cad.eecs.berkeley.edu\/~kenmcmil\/smv\/."},{"key":"e_1_2_1_6_1","unstructured":"Clarke E. M. Grumberg O. and Peled D. A. 1999. Model Checking. MIT Press Cambridge MA.   Clarke E. M. Grumberg O. and Peled D. A. 1999. Model Checking. MIT Press Cambridge MA."},{"key":"e_1_2_1_7_1","volume-title":"Proceedings of the 13th International Symposium on System Level Synthesis (ISSS)","author":"Cort\u00e9s L. A.","year":"1822","unstructured":"Cort\u00e9s , L. A. , Eles , P. , and Peng , Z . 2000. Verification of Embedded Systems using a Petri Net based Representation . In Proceedings of the 13th International Symposium on System Level Synthesis (ISSS) . Madrid, Spain. 149--155. 10.1145\/501790.50 1822 Cort\u00e9s, L. A., Eles, P., and Peng, Z. 2000. Verification of Embedded Systems using a Petri Net based Representation. In Proceedings of the 13th International Symposium on System Level Synthesis (ISSS). Madrid, Spain. 149--155. 10.1145\/501790.501822"},{"key":"e_1_2_1_8_1","volume-title":"Proceedings of the 31st Conference on Union of Bulgarian's mathematicians","author":"Dimiev S.","unstructured":"Dimiev , S. and Markov , K . 2002. Gauss Integers and Diophantine Figures . In Proceedings of the 31st Conference on Union of Bulgarian's mathematicians . Borovetz, Bulgaria. Dimiev, S. and Markov, K. 2002. Gauss Integers and Diophantine Figures. In Proceedings of the 31st Conference on Union of Bulgarian's mathematicians. Borovetz, Bulgaria."},{"key":"e_1_2_1_9_1","volume-title":"Proceedings of the 1st Design, Automation and Test in Europe (DATE)","author":"Eles P.","unstructured":"Eles , P. , Kuchcinski , K. , Peng , Z. , Doboli , A. , and Pop , P . 1998. Scheduling of conditional process graphs for the synthesis of embedded systems . In Proceedings of the 1st Design, Automation and Test in Europe (DATE) . Paris, France. Eles, P., Kuchcinski, K., Peng, Z., Doboli, A., and Pop, P. 1998. Scheduling of conditional process graphs for the synthesis of embedded systems. In Proceedings of the 1st Design, Automation and Test in Europe (DATE). Paris, France."},{"key":"e_1_2_1_10_1","first-page":"995","article-title":"Temporal and Modal Logic. In Handbook of Theoretical Computer Science, J. van Leeuwen, Ed. vol. B: Formal Models and Semantics. Elseiver Science, New York","volume":"16","author":"Emerson E. A.","year":"1990","unstructured":"Emerson , E. A. 1990 . Temporal and Modal Logic. In Handbook of Theoretical Computer Science, J. van Leeuwen, Ed. vol. B: Formal Models and Semantics. Elseiver Science, New York , Chapter 16 , 995 -- 1072 . Emerson, E. A. 1990. Temporal and Modal Logic. In Handbook of Theoretical Computer Science, J. van Leeuwen, Ed. vol. B: Formal Models and Semantics. Elseiver Science, New York, Chapter 16, 995--1072.","journal-title":"Chapter"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/4904.4999"},{"key":"e_1_2_1_13_1","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1016\/0304-3975(85)90014-3","article-title":"An Introduction to FIFO nets --Monogeneous nets: A subclass of FIFO nets","volume":"35","author":"Finkel A.","year":"1985","unstructured":"Finkel , A. and Memmi , G. 1985 . An Introduction to FIFO nets --Monogeneous nets: A subclass of FIFO nets . Theoret. Computer Sci. 35 , 191 -- 214 . Finkel, A. and Memmi, G. 1985. An Introduction to FIFO nets --Monogeneous nets: A subclass of FIFO nets. Theoret. Computer Sci. 35, 191--214.","journal-title":"Theoret. Computer Sci."},{"key":"e_1_2_1_14_1","volume-title":"1987. Silicon Compilers. Addison--Wesley","author":"Gajski D. D.","unstructured":"Gajski , D. D. , Ed. 1987. Silicon Compilers. Addison--Wesley , Reading, MA . Gajski, D. D., Ed. 1987. Silicon Compilers. Addison--Wesley, Reading, MA."},{"key":"e_1_2_1_15_1","volume-title":"Principles of Digital Design","author":"Gajski D. D.","unstructured":"Gajski , D. D. 1997. Principles of Digital Design . Prentice-Hall , Englewood Cliff, NJ . Gajski, D. D. 1997. Principles of Digital Design. Prentice-Hall, Englewood Cliff, NJ."},{"key":"e_1_2_1_16_1","volume-title":"Advances in Petri Nets 1986 Part I: Petri Nets, central models and their properties","author":"Genrich H.","unstructured":"Genrich , H. 1987. Predicate \/Transition-Nets. In Advances in Petri Nets 1986 Part I: Petri Nets, central models and their properties , W. Brauer, W. Reisig, and G. Rozenberg, Eds. Lecture Notes in Computer Science, vol. 254 . Springer-Verlag . 207--247. Genrich, H. 1987. Predicate\/Transition-Nets. In Advances in Petri Nets 1986 Part I: Petri Nets, central models and their properties, W. Brauer, W. Reisig, and G. Rozenberg, Eds. Lecture Notes in Computer Science, vol. 254. Springer-Verlag. 207--247."},{"key":"e_1_2_1_17_1","series-title":"Electronic Sciences Series","volume-title":"Introduction to the Theory of Finite-State Machines","author":"Gill A.","unstructured":"Gill , A. 1962. Introduction to the Theory of Finite-State Machines . Electronic Sciences Series . McGraw-Hill , New York , 10020. Gill, A. 1962. Introduction to the Theory of Finite-State Machines. Electronic Sciences Series. McGraw-Hill, New York, 10020."},{"key":"e_1_2_1_18_1","volume-title":"International Symposium on High Performance Computing.","author":"Grode J.","unstructured":"Grode , J. , Madsen , J. , and Jerraya , A . -A. 1998. Performance Estimation for Hardware\/Software Codesign using Hierarchical Colored Petri Nets . In International Symposium on High Performance Computing. Grode, J., Madsen, J., and Jerraya, A.-A. 1998. Performance Estimation for Hardware\/Software Codesign using Hierarchical Colored Petri Nets. In International Symposium on High Performance Computing."},{"key":"e_1_2_1_20_1","unstructured":"Jensen K. 1992. Coloured Petri Nets---Basic Concepts Analysis Methods and Practical Use. EATCS Monographs in Theoretical Computer Science 1 Basic Concepts 1--234.   Jensen K. 1992. Coloured Petri Nets---Basic Concepts Analysis Methods and Practical Use. EATCS Monographs in Theoretical Computer Science 1 Basic Concepts 1--234."},{"key":"e_1_2_1_21_1","unstructured":"Jensen K. 1994. Coloured Petri Nets---Basic Concepts Analysis Methods and Practical Use. EATCS Monographs in Theoretical Computer Science 2 Analysis Methods.   Jensen K. 1994. Coloured Petri Nets---Basic Concepts Analysis Methods and Practical Use. EATCS Monographs in Theoretical Computer Science 2 Analysis Methods."},{"key":"e_1_2_1_22_1","doi-asserted-by":"crossref","unstructured":"Jensen K. 1997. Coloured Petri Nets---Basic Concepts Analysis Methods and Practical Use. EATCS Monographs in Theoretical Computer Science 3 Practical Use.   Jensen K. 1997. Coloured Petri Nets---Basic Concepts Analysis Methods and Practical Use. EATCS Monographs in Theoretical Computer Science 3 Practical Use.","DOI":"10.1007\/978-3-642-60794-3"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/307988.307989"},{"key":"e_1_2_1_24_1","volume-title":"Proceedings of the 13th IFIP WG 10.5 Conference on Computer Hardware Description Languages and Their Applications (CHDL)","author":"Kleinjohann B.","unstructured":"Kleinjohann , B. , Tacken , J. , and Tahedl , C . 1997. Towards a Complete Design Method for Embedded Systems Using Predicate\/Transition-Nets . In Proceedings of the 13th IFIP WG 10.5 Conference on Computer Hardware Description Languages and Their Applications (CHDL) . Toledo, Spain. Kleinjohann, B., Tacken, J., and Tahedl, C. 1997. Towards a Complete Design Method for Embedded Systems Using Predicate\/Transition-Nets. In Proceedings of the 13th IFIP WG 10.5 Conference on Computer Hardware Description Languages and Their Applications (CHDL). Toledo, Spain."},{"key":"e_1_2_1_25_1","volume-title":"On the Complexity of Branching Modular Model Checking. In 6th International Conference on Concurrency Theory (CONCUR)","author":"Kupferman O.","unstructured":"Kupferman , O. and Vardi , M. Y . 1995 . On the Complexity of Branching Modular Model Checking. In 6th International Conference on Concurrency Theory (CONCUR) . Philadelphia, Pennsylvania. Kupferman, O. and Vardi, M. Y. 1995. On the Complexity of Branching Modular Model Checking. In 6th International Conference on Concurrency Theory (CONCUR). Philadelphia, Pennsylvania."},{"key":"e_1_2_1_26_1","first-page":"9","article-title":"Synchronous Dataflow","volume":"75","author":"Lee E. A.","year":"1987","unstructured":"Lee , E. A. and Messerschmitt , D. G. 1987 . Synchronous Dataflow . Proceedings of the IEEE 75 , 9 (Sept.), 1235--1245. Lee, E. A. and Messerschmitt, D. G. 1987. Synchronous Dataflow. Proceedings of the IEEE 75, 9 (Sept.), 1235--1245.","journal-title":"Proceedings of the IEEE"},{"key":"e_1_2_1_27_1","volume-title":"Symbolic Model Checking","author":"McMillan K. L.","unstructured":"McMillan , K. L. 1993. Symbolic Model Checking . Kluwer Academic Pub , Boston, MA . McMillan, K. L. 1993. Symbolic Model Checking. Kluwer Academic Pub, Boston, MA."},{"key":"e_1_2_1_28_1","doi-asserted-by":"crossref","first-page":"1036","DOI":"10.1109\/TCOM.1976.1093424","article-title":"Recoverability of Communication Protocols","volume":"24","author":"Merlin P.","year":"1976","unstructured":"Merlin , P. and Faber , D. J. 1976 . Recoverability of Communication Protocols . IEEE Transaction on Communications 24 , 9, 1036 -- 1043 . Merlin, P. and Faber, D. J. 1976. Recoverability of Communication Protocols. IEEE Transaction on Communications 24, 9, 1036--1043.","journal-title":"IEEE Transaction on Communications"},{"key":"e_1_2_1_29_1","doi-asserted-by":"crossref","first-page":"4","DOI":"10.1109\/5.24143","article-title":"Petri Nets: Properties, Analysis and Applications","volume":"77","author":"Murata T.","year":"1989","unstructured":"Murata , T. 1989 . Petri Nets: Properties, Analysis and Applications . Proceedings of the IEEE 77 , 4 (Apr.), 541--580. Murata, T. 1989. Petri Nets: Properties, Analysis and Applications. Proceedings of the IEEE 77, 4 (Apr.), 541--580.","journal-title":"Proceedings of the IEEE"},{"key":"e_1_2_1_30_1","volume-title":"Proceedings of the 6th International Conference on Computer Aided Verification. Lecture Notes in Computer Science","volume":"818","author":"Naik V. G.","unstructured":"Naik , V. G. and Sistla , A. P . 1994. Modeling and Verification of a Real Life Protocol Using Symbolic Model Checking . In Proceedings of the 6th International Conference on Computer Aided Verification. Lecture Notes in Computer Science , vol. 818 . Stanford, CA. Naik, V. G. and Sistla, A. P. 1994. Modeling and Verification of a Real Life Protocol Using Symbolic Model Checking. In Proceedings of the 6th International Conference on Computer Aided Verification. Lecture Notes in Computer Science, vol. 818. Stanford, CA."},{"key":"e_1_2_1_31_1","volume-title":"Technical Report ICS-TR-90-20, University of California, Irvine, Department of Information and Computer Science. Oct.","author":"Narayan S.","year":"1992","unstructured":"Narayan , S. and Vahid , F . 1992 . Modeling with SpecCharts . Technical Report ICS-TR-90-20, University of California, Irvine, Department of Information and Computer Science. Oct. Narayan, S. and Vahid, F. 1992. Modeling with SpecCharts. Technical Report ICS-TR-90-20, University of California, Irvine, Department of Information and Computer Science. Oct."},{"key":"e_1_2_1_32_1","volume-title":"Proceedings of the APCHDL'97","author":"\u00d6sterling A.","unstructured":"\u00d6sterling , A. , Benner , T. , and Ernst , R . 1997. Code Generation and Context Switching for Static Scheduling of Mixed Control and Data Oriented HW\/SW Systems . In Proceedings of the APCHDL'97 . Taiwan. 131--135. \u00d6sterling, A., Benner, T., and Ernst, R. 1997. Code Generation and Context Switching for Static Scheduling of Mixed Control and Data Oriented HW\/SW Systems. In Proceedings of the APCHDL'97. Taiwan. 131--135."},{"key":"e_1_2_1_34_1","first-page":"2","article-title":"Automated Transformation of Algorithms into Register-Transfer Level Implementations","volume":"13","author":"Peng Z.","year":"1994","unstructured":"Peng , Z. and Kuchcinski , K. 1994 . Automated Transformation of Algorithms into Register-Transfer Level Implementations . IEEE Transaction on Computer-Aided Design of Integrated Circuits and Systems 13 , 2 (Feb.), 150--166. Peng, Z. and Kuchcinski, K. 1994. Automated Transformation of Algorithms into Register-Transfer Level Implementations. IEEE Transaction on Computer-Aided Design of Integrated Circuits and Systems 13, 2 (Feb.), 150--166.","journal-title":"IEEE Transaction on Computer-Aided Design of Integrated Circuits and Systems"},{"key":"e_1_2_1_35_1","volume-title":"12th International Colloquium on Automata, Languages, and Programming","author":"Pnueli A.","unstructured":"Pnueli , A. 1985. Linear and Branching Structures in the Semantics and Logics of Reactive Systems . In 12th International Colloquium on Automata, Languages, and Programming . Springer-Verlag , Berlin , 15--32. Pnueli, A. 1985. Linear and Branching Structures in the Semantics and Logics of Reactive Systems. In 12th International Colloquium on Automata, Languages, and Programming. Springer-Verlag, Berlin, 15--32."},{"key":"e_1_2_1_36_1","volume-title":"Eds","author":"Staunstrup J.","year":"1997","unstructured":"Staunstrup , J. and Wolf , W. , Eds . 1997 . Hardware\/Software Co-Design: Principles and Practice. Kluwer Academic Publishers , Dordrecht, The Netherlands. Staunstrup, J. and Wolf, W., Eds. 1997. Hardware\/Software Co-Design: Principles and Practice. Kluwer Academic Publishers, Dordrecht, The Netherlands."},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1109\/92.931229"},{"key":"e_1_2_1_38_1","volume-title":"European Joint Conference on Theory and Practice of Software","author":"Vardi M. Y.","year":"2001","unstructured":"Vardi , M. Y. 2001 . Branching vs. linear time: Final showdown . In European Joint Conference on Theory and Practice of Software . Genova, Italy. Vardi, M. Y. 2001. Branching vs. linear time: Final showdown. In European Joint Conference on Theory and Practice of Software. Genova, Italy."},{"key":"e_1_2_1_39_1","first-page":"8","article-title":"Formal Verification of Timed Systems: A Survey and Perspective","volume":"92","author":"Wang F.","year":"2004","unstructured":"Wang , F. 2004 . Formal Verification of Timed Systems: A Survey and Perspective . Proceedings of the IEEE 92 , 8 (Aug.), 1283--1305. Wang, F. 2004. Formal Verification of Timed Systems: A Survey and Perspective. Proceedings of the IEEE 92, 8 (Aug.), 1283--1305.","journal-title":"Proceedings of the IEEE"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1109\/MC.2003.1193227"},{"key":"e_1_2_1_41_1","volume-title":"Proceedings of the GI\/ITG\/GMM Workshop \u201cEntwurfsmethoden & Beschreibungssprachen.&rdquo;\u201d Braunschweig, Germany.","author":"Ziegenbein D.","unstructured":"Ziegenbein , D. , Richter , K. , Ernst , R. , Thiele , L. , and Teich , J . 1999. SPI---An Internal Representation for Heterogeneously Specified Embedded Systems . In Proceedings of the GI\/ITG\/GMM Workshop \u201cEntwurfsmethoden & Beschreibungssprachen.&rdquo;\u201d Braunschweig, Germany. Ziegenbein, D., Richter, K., Ernst, R., Thiele, L., and Teich, J. 1999. SPI---An Internal Representation for Heterogeneously Specified Embedded Systems. In Proceedings of the GI\/ITG\/GMM Workshop \u201cEntwurfsmethoden & Beschreibungssprachen.&rdquo;\u201d Braunschweig, Germany."}],"container-title":["ACM Transactions on Embedded Computing Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1132357.1132360","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1132357.1132360","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T16:18:50Z","timestamp":1750263530000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1132357.1132360"}},"subtitle":["Modeling the control\/data-flow relation in embedded systems"],"short-title":[],"issued":{"date-parts":[[2006,2]]},"references-count":37,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2006,2]]}},"alternative-id":["10.1145\/1132357.1132360"],"URL":"https:\/\/doi.org\/10.1145\/1132357.1132360","relation":{},"ISSN":["1539-9087","1558-3465"],"issn-type":[{"value":"1539-9087","type":"print"},{"value":"1558-3465","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006,2]]},"assertion":[{"value":"2006-02-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}