{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,1]],"date-time":"2026-05-01T18:04:14Z","timestamp":1777658654147,"version":"3.51.4"},"reference-count":43,"publisher":"Elsevier BV","issue":"12-15","license":[{"start":{"date-parts":[[2003,12,1]],"date-time":"2003-12-01T00:00:00Z","timestamp":1070236800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Journal of Systems Architecture"],"published-print":{"date-parts":[[2003,12]]},"DOI":"10.1016\/s1383-7621(03)00096-1","type":"journal-article","created":{"date-parts":[[2003,9,12]],"date-time":"2003-09-12T05:07:29Z","timestamp":1063343249000},"page":"571-598","source":"Crossref","is-referenced-by-count":40,"title":["Modeling and formal verification of embedded systems based on a Petri net representation"],"prefix":"10.1016","volume":"49","author":[{"given":"Luis Alejandro","family":"Cort\u00e9s","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Petru","family":"Eles","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zebo","family":"Peng","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/S1383-7621(03)00096-1_BIB1","doi-asserted-by":"crossref","unstructured":"R. Alur, C. Courcoubetis, D.L. Dill, Model checking for real-time systems, in: Proc. Symposium on Logic in Computer Science, 1990, pp. 414\u2013425","DOI":"10.1109\/LICS.1990.113766"},{"key":"10.1016\/S1383-7621(03)00096-1_BIB2","doi-asserted-by":"crossref","unstructured":"F. Balarin, H. Hsieh, A. Jurecska, L. Lavagno, A. Sangiovanni-Vincentelli, Formal verification of embedded systems based on CFSM networks, in: Proc. DAC, 1996, pp. 568\u2013571","DOI":"10.1145\/240518.240626"},{"issue":"4","key":"10.1016\/S1383-7621(03)00096-1_BIB3","doi-asserted-by":"crossref","first-page":"251","DOI":"10.1145\/359094.359101","article-title":"New methods to color the vertices of a graph","volume":"22","author":"Br\u00e9laz","year":"1979","journal-title":"Communications of the ACM"},{"issue":"January","key":"10.1016\/S1383-7621(03)00096-1_BIB4","doi-asserted-by":"crossref","first-page":"5","DOI":"10.1007\/BF00134682","article-title":"Embedded system design","volume":"1","author":"Camposano","year":"1996","journal-title":"Design Automation for Embedded Systems"},{"issue":"August","key":"10.1016\/S1383-7621(03)00096-1_BIB5","doi-asserted-by":"crossref","first-page":"117","DOI":"10.1016\/0304-3975(94)00231-7","article-title":"Complexity results for 1-safe nets","volume":"147","author":"Cheng","year":"1995","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/S1383-7621(03)00096-1_BIB6","unstructured":"M. Chiodo, P. Giusto, H. Hsieh, A. Jurecska, L. Lavagno, A. Sangiovanni-Vincentelli, A formal specification model for hardware\/software codesign, Technical Report UCB\/ERL M93\/48, Dept. EECS, University of California, Berkeley, June 1993"},{"issue":"2","key":"10.1016\/S1383-7621(03)00096-1_BIB7","doi-asserted-by":"crossref","first-page":"244","DOI":"10.1145\/5397.5399","article-title":"Automatic verification of finite-state concurrent systems using temporal logic specifications","volume":"8","author":"Clarke","year":"1986","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"10.1016\/S1383-7621(03)00096-1_BIB8","series-title":"Model Checking","author":"Clarke","year":"1999"},{"key":"10.1016\/S1383-7621(03)00096-1_BIB9","unstructured":"L.A. Cort\u00e9s, A Petri net based modeling and verification technique for real-time embedded systems, Licentiate Thesis, Dept. of Computer and Information Science, Link\u00f6ping University, Link\u00f6ping, 2001"},{"key":"10.1016\/S1383-7621(03)00096-1_BIB10","doi-asserted-by":"crossref","unstructured":"L.A. Cort\u00e9s, P. Eles, Z. Peng, Definitions of equivalence for transformational synthesis of embedded systems, in: Proc. ICECCS, 2000, pp. 134\u2013142","DOI":"10.1109\/ICECCS.2000.873937"},{"key":"10.1016\/S1383-7621(03)00096-1_BIB11","doi-asserted-by":"crossref","unstructured":"L.A. Cort\u00e9s, P. Eles, Z. Peng, Verification of embedded systems using a Petri net based representation, in: Proc. ISSS, 2000, pp. 149\u2013155","DOI":"10.1109\/ISSS.2000.874042"},{"key":"10.1016\/S1383-7621(03)00096-1_BIB12","doi-asserted-by":"crossref","unstructured":"L.A. Cort\u00e9s, P. Eles, Z. Peng, Hierarchical modeling and verification of embedded systems, in: Proc. Euromicro Symposium on Digital System Design, 2001, pp. 63\u201370","DOI":"10.1109\/DSD.2001.952119"},{"key":"10.1016\/S1383-7621(03)00096-1_BIB13","doi-asserted-by":"crossref","first-page":"366","DOI":"10.1109\/5.558710","article-title":"Design of embedded systems: formal models, validation, and synthesis","volume":"85","author":"Edwards","year":"1997","journal-title":"Proc. IEEE"},{"key":"10.1016\/S1383-7621(03)00096-1_BIB14","doi-asserted-by":"crossref","unstructured":"P. Eles, K. Kuchcinski, Z. Peng, A. Doboli, P. Pop, Scheduling of conditional process graphs for the synthesis of embedded systems, in: Proc. DATE Conference, 1998, pp. 132\u2013138","DOI":"10.1109\/DATE.1998.655847"},{"key":"10.1016\/S1383-7621(03)00096-1_BIB15","series-title":"Lectures on Petri Nets: Basic Models, LNCS 1491","first-page":"374","article-title":"Decidability and complexity of Petri net problems\u2013\u2013an introduction","author":"Esparza","year":"1998"},{"issue":"3","key":"10.1016\/S1383-7621(03)00096-1_BIB16","doi-asserted-by":"crossref","first-page":"171","DOI":"10.1049\/ip-cdt:19981973","article-title":"CodeSign: An embedded system design environment","volume":"145","author":"Esser","year":"1998","journal-title":"IEE Proc. Computers and Digital Techniques"},{"issue":"4","key":"10.1016\/S1383-7621(03)00096-1_BIB17","doi-asserted-by":"crossref","first-page":"44","DOI":"10.1109\/54.329454","article-title":"Introduction to high-level synthesis","volume":"11","author":"Gajski","year":"1994","journal-title":"IEEE Design & Test of Computers"},{"key":"10.1016\/S1383-7621(03)00096-1_BIB18","series-title":"Software Specification: A Comparison of Formal Methods","author":"Gannon","year":"1994"},{"key":"10.1016\/S1383-7621(03)00096-1_BIB19","series-title":"Computers and Intractability: A Guide to the Theory of NP-Completeness","author":"Garey","year":"1979"},{"issue":"3","key":"10.1016\/S1383-7621(03)00096-1_BIB20","doi-asserted-by":"crossref","first-page":"231","DOI":"10.1016\/0167-6423(87)90035-9","article-title":"Statecharts: A visual formalism for complex systems","volume":"8","author":"Harel","year":"1987","journal-title":"Science of Computer Programming"},{"key":"10.1016\/S1383-7621(03)00096-1_BIB21","series-title":"Introduction to Automata Theory, Languages, Computation","author":"Hopcroft","year":"2001"},{"key":"10.1016\/S1383-7621(03)00096-1_BIB22","unstructured":"HyTech. Available from <http:\/\/www-cad.eecs.berkeley.edu\/~tah\/HyTech>"},{"key":"10.1016\/S1383-7621(03)00096-1_BIB23","series-title":"Coloured Petri Nets","author":"Jensen","year":"1992"},{"issue":"2","key":"10.1016\/S1383-7621(03)00096-1_BIB24","doi-asserted-by":"crossref","first-page":"123","DOI":"10.1145\/307988.307989","article-title":"Formal verification in hardware design: A survey","volume":"4","author":"Kern","year":"1999","journal-title":"ACM Trans. on Design Automation of Electronic Systems"},{"key":"10.1016\/S1383-7621(03)00096-1_BIB25","unstructured":"A. Kovalyov, J. Esparza, A polynomial algorithm to compute the concurrency relation of free-choice Signal Transition Graphs, in: Proc. Intl. Workshop on Discrete Event Systems, 1996, pp. 1\u20136"},{"key":"10.1016\/S1383-7621(03)00096-1_BIB26","unstructured":"Kronos. Available from <http:\/\/www-verimag.imag.fr\/TEMPORISE\/kronos>"},{"key":"10.1016\/S1383-7621(03)00096-1_BIB27","series-title":"System-Level Synthesis","first-page":"45","article-title":"Models of computation for embedded system design","author":"Lavagno","year":"1999"},{"issue":"5","key":"10.1016\/S1383-7621(03)00096-1_BIB28","doi-asserted-by":"crossref","first-page":"773","DOI":"10.1109\/5.381846","article-title":"Dataflow process networks","volume":"83","author":"Lee","year":"1995","journal-title":"Proc. IEEE"},{"key":"10.1016\/S1383-7621(03)00096-1_BIB29","unstructured":"P. Lind, S. Kvist, Jammer model description, Technical report, Saab Bofors Dynamics AB, Link\u00f6ping, April 2001"},{"issue":"4","key":"10.1016\/S1383-7621(03)00096-1_BIB30","doi-asserted-by":"crossref","first-page":"243","DOI":"10.1023\/A:1008969621405","article-title":"A Petri net model for hardware\/software codesign","volume":"4","author":"Maciel","year":"1999","journal-title":"Design Automation for Embedded Systems"},{"issue":"9","key":"10.1016\/S1383-7621(03)00096-1_BIB31","doi-asserted-by":"crossref","first-page":"1036","DOI":"10.1109\/TCOM.1976.1093424","article-title":"Recoverability of communication protocols\u2013\u2013implications of a theoretical study","volume":"24","author":"Merlin","year":"1976","journal-title":"IEEE Trans. Communications, COM"},{"issue":"4","key":"10.1016\/S1383-7621(03)00096-1_BIB32","doi-asserted-by":"crossref","first-page":"541","DOI":"10.1109\/5.24143","article-title":"Petri nets: analysis and applications","volume":"77","author":"Murata","year":"1989","journal-title":"Proc. IEEE"},{"key":"10.1016\/S1383-7621(03)00096-1_BIB33","series-title":"Petri Net Theory and the Modeling of Systems","author":"Peterson","year":"1981"},{"key":"10.1016\/S1383-7621(03)00096-1_BIB34","unstructured":"C. Ramchandani, Analysis of asynchronous concurrent systems by timed Petri nets, Technical Report Project MAC 120, Massachusetts Institute of Technology, Cambridge, February 1974"},{"key":"10.1016\/S1383-7621(03)00096-1_BIB35","doi-asserted-by":"crossref","unstructured":"M. Sgroi, L. Lavagno, Y. Watanabe, A. Sangiovanni-Vincentelli, Synthesis of embedded software using free-choice Petri nets, in: Proc. DAC, 1999, pp. 805\u2013810","DOI":"10.1145\/309847.310073"},{"key":"10.1016\/S1383-7621(03)00096-1_BIB36","series-title":"Net Theory and Applications, LNCS 84","first-page":"307","article-title":"Performance evaluation of systems using nets","author":"Sifakis","year":"1980"},{"key":"10.1016\/S1383-7621(03)00096-1_BIB37","unstructured":"E. Stoy, A Petri net based unified representation for hardware\/software co-design, Licentiate Thesis, Dept. of Computer and Information Science, Link\u00f6ping University, Link\u00f6ping, 1995"},{"issue":"4","key":"10.1016\/S1383-7621(03)00096-1_BIB38","doi-asserted-by":"crossref","first-page":"524","DOI":"10.1109\/92.931229","article-title":"FunState\u2013\u2013An internal design representation for codesign","volume":"9","author":"Strehl","year":"2001","journal-title":"IEEE Trans. VLSI Systems"},{"key":"10.1016\/S1383-7621(03)00096-1_BIB39","unstructured":"The SAVE Project. Available from <http:\/\/www.ida.liu.se\/~eslab\/save.shtml>"},{"key":"10.1016\/S1383-7621(03)00096-1_BIB40","unstructured":"Uppaal. Available from <http:\/\/www.uppaal.com>"},{"key":"10.1016\/S1383-7621(03)00096-1_BIB41","doi-asserted-by":"crossref","unstructured":"M. Varea, B. Al-Hashimi, Dual transitions Petri net based modelling technique for embedded systems specification, in: Proc. DATE Conference, 2001, pp. 566\u2013571","DOI":"10.1109\/DATE.2001.915080"},{"key":"10.1016\/S1383-7621(03)00096-1_BIB42","doi-asserted-by":"crossref","unstructured":"M. Varea, B. Al-Hashimi, L.A. Cort\u00e9s, P. Eles, Z. Peng, Symbolic model checking of dual transition Petri nets, in: Proc. CODES, 2002, pp. 43\u201348","DOI":"10.1145\/774789.774799"},{"key":"10.1016\/S1383-7621(03)00096-1_BIB43","doi-asserted-by":"crossref","first-page":"71","DOI":"10.1016\/0020-0190(91)90225-7","article-title":"A polynomial time algorithm to decide pairwise concurrency of transitions for 1-bounded conflict-free Petri nets","volume":"38","author":"Yen","year":"1991","journal-title":"Information Processing Letters"}],"container-title":["Journal of Systems Architecture"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1383762103000961?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1383762103000961?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2020,3,25]],"date-time":"2020-03-25T13:51:02Z","timestamp":1585144262000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S1383762103000961"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,12]]},"references-count":43,"journal-issue":{"issue":"12-15","published-print":{"date-parts":[[2003,12]]}},"alternative-id":["S1383762103000961"],"URL":"https:\/\/doi.org\/10.1016\/s1383-7621(03)00096-1","relation":{},"ISSN":["1383-7621"],"issn-type":[{"value":"1383-7621","type":"print"}],"subject":[],"published":{"date-parts":[[2003,12]]}}}