{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,19]],"date-time":"2025-03-19T15:13:12Z","timestamp":1742397192903,"version":"3.30.1"},"reference-count":27,"publisher":"Elsevier BV","issue":"15","license":[{"start":{"date-parts":[[2000,12,1]],"date-time":"2000-12-01T00:00:00Z","timestamp":975628800000},"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":[[2000,12]]},"DOI":"10.1016\/s1383-7621(00)00034-5","type":"journal-article","created":{"date-parts":[[2003,4,7]],"date-time":"2003-04-07T18:33:56Z","timestamp":1049740436000},"page":"1435-1450","source":"Crossref","is-referenced-by-count":25,"title":["Embedded software verification in hardware\u2013software codesign"],"prefix":"10.1016","volume":"46","author":[{"given":"Pao-Ann","family":"Hsiung","sequence":"first","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/S1383-7621(00)00034-5_BIB1","doi-asserted-by":"crossref","unstructured":"M. Abadi, L. Lamport, An old-fashioned recipe for real time, in: REX Workshop, Real-Time Theory in Practice, Lecture Notes in Computer Science, vol. 600, June 1991, pp. 1\u201327","DOI":"10.1007\/BFb0031985"},{"key":"10.1016\/S1383-7621(00)00034-5_BIB2","doi-asserted-by":"crossref","unstructured":"K. Altisen, G. Gobler, A. Pneuli, J. Sifakis, S. Tripakis, S. Yovine, A framework for scheduler synthesis, in: Real-Time System Symposium (RTSS'99), IEEE Computer Society Press, 1999","DOI":"10.1109\/REAL.1999.818838"},{"key":"10.1016\/S1383-7621(00)00034-5_BIB3","doi-asserted-by":"crossref","unstructured":"R. Alur, C. Courcoubetis, D. Dill, N. Halbwachs, H. Wong-Toi, An implementation of three algorithms for timing verification based on automata emptiness, in: Proceedings of IEEE International Conference on Real-Time Systems Symposium (RTSS'92), 1992","DOI":"10.1109\/REAL.1992.242667"},{"key":"10.1016\/S1383-7621(00)00034-5_BIB4","doi-asserted-by":"crossref","unstructured":"R. Alur, C. Courcoubetis, N. Halbwachs, D. Dill, Model checking for real-time systems, in: Proceedings of IEEE Logics in Computer Science, 1990","DOI":"10.1109\/LICS.1990.113766"},{"key":"10.1016\/S1383-7621(00)00034-5_BIB5","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/0304-3975(94)00202-T","article-title":"The algorithmic analysis of hybrid systems","volume":"138","author":"Alur","year":"1995","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/S1383-7621(00)00034-5_BIB6","doi-asserted-by":"crossref","unstructured":"R. Alur, C. Courcoubetis, T. Henzinger, P.-H. Ho, Hybrid automata: an algorithmic approach to the specification and verification of hybrid systems, in: R. Grossman, A. Nerode, A. Raun, H. Rischel (Eds.), Hybrid Systems, vol. 736, Lecture Notes in Computer Science, Springer, Berlin, 1993, pp. 209\u2013229","DOI":"10.1007\/3-540-57318-6_30"},{"issue":"2","key":"10.1016\/S1383-7621(00)00034-5_BIB7","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","article-title":"Automata for modeling real-time systems","volume":"126","author":"Alur","year":"1994","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/S1383-7621(00)00034-5_BIB8","doi-asserted-by":"crossref","unstructured":"E. Asarin, O. Maler, A. Pneuli. Symbolic controller synthesis for discrete and timed systems, in: P. Antsaklis, W. Kohn, A. Nerode, S. Sastry (Eds.), Hybrid Systems II, vol. 999, Lecture Notes in Computer Science, Springer, Berlin, 1995, pp. 1\u201320","DOI":"10.1007\/3-540-60472-3_1"},{"key":"10.1016\/S1383-7621(00)00034-5_BIB9","doi-asserted-by":"crossref","unstructured":"E. Asarin, O. Maler, A. Pneuli, J. Sifakis, Controller synthesis for timed automata, in: Proceedings of the System Structure and Control, IFAC, Elsevier, July 1998","DOI":"10.1016\/S1474-6670(17)42032-5"},{"key":"10.1016\/S1383-7621(00)00034-5_BIB10","doi-asserted-by":"crossref","unstructured":"F. Balarin, M. Chiodo, Software synthesis for complex reactive embedded systems, in: Proceedings of International Conference on Computer Design (ICCD'99), IEEE CS Press, October 1999, pp. 634\u2013639","DOI":"10.1109\/ICCD.1999.808608"},{"year":"1997","series-title":"Hardware\u2013software Co-design of Embedded Systems: the POLIS approach","author":"Balarin","key":"10.1016\/S1383-7621(00)00034-5_BIB11"},{"issue":"8","key":"10.1016\/S1383-7621(00)00034-5_BIB12","doi-asserted-by":"crossref","DOI":"10.1109\/TC.1986.1676819","article-title":"Graph-based algorithms for boolean function manipulation","volume":"C-35","author":"Bryant","year":"1986","journal-title":"IEEE Transactions on Computers"},{"key":"10.1016\/S1383-7621(00)00034-5_BIB13","doi-asserted-by":"crossref","unstructured":"D. Dill, Timing assumptions and verification of finite-state concurrent systems, in: Proceedings of the International Conference on Computer-Aided Verification, LNCS, vol. 407, Springer, Berlin, 1989","DOI":"10.1007\/3-540-52148-8_17"},{"key":"10.1016\/S1383-7621(00)00034-5_BIB14","doi-asserted-by":"crossref","unstructured":"E. Emerson, Temporal and modal logic, Handbook of Theoretical Computer Science, 1990","DOI":"10.1016\/B978-0-444-88074-1.50021-4"},{"key":"10.1016\/S1383-7621(00)00034-5_BIB15","doi-asserted-by":"crossref","unstructured":"T. Henzinger, X. Nicollin, J. Sifakis, S. Yovine, Symbolic model checking for real-time systems, in: Proceedings of the IEEE Logics in Computer Science, 1992","DOI":"10.1109\/LICS.1992.185551"},{"key":"10.1016\/S1383-7621(00)00034-5_BIB16","doi-asserted-by":"crossref","unstructured":"P.-A. Hsiung, Timing coverification of concurrent embedded real-time systems, in: Proceedings of the Seventh IEEE\/ACM International Workshop on Hardware Software Codesign (CODES'99), ACM Press, New York, May 1999, pp. 110\u2013114","DOI":"10.1145\/301177.301501"},{"key":"10.1016\/S1383-7621(00)00034-5_BIB17","doi-asserted-by":"crossref","unstructured":"P.-A. Hsiung, F. Wang, A state-graph manipulator tool for real-time system specification and verification, in: Proceedings of the Fourth International Conference on Real-Time Computing Systems and Applications (RTCSA'98), IEEE Computer Society Press, October 1998, pp. 181\u2013188","DOI":"10.1109\/RTCSA.1998.726415"},{"key":"10.1016\/S1383-7621(00)00034-5_BIB18","doi-asserted-by":"crossref","unstructured":"P.-A. Hsiung, F. Wang, User-friendly verification, in: International Conference on Formal Description Techniques For Distributed Systems and Communication Protocols & Protocol Specification, Testing, and Verification (FORTE\/PSTV'99), October 1999","DOI":"10.1007\/978-0-387-35578-8_16"},{"issue":"1","key":"10.1016\/S1383-7621(00)00034-5_BIB19","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/7351.7352","article-title":"A fast mutual exclusion algorithm","volume":"5","author":"Lamport","year":"1987","journal-title":"ACM Transactions on Computer Systems"},{"key":"10.1016\/S1383-7621(00)00034-5_BIB20","doi-asserted-by":"crossref","unstructured":"K.G. Larsen, B. Steffen, C. Weise, Fischer's protocol revisited: a simple proof using modal constraints, in: Hybrid System III, Lecture Notes in Computer Science, vol. 1066, 1996, pp. 604\u2013615","DOI":"10.1007\/BFb0020979"},{"key":"10.1016\/S1383-7621(00)00034-5_BIB21","doi-asserted-by":"crossref","unstructured":"B. Lin, Efficient compilation of process-based concurrent programs without run-time scheduling, in: Proceedings of Design Automation and Test Europe (DATE'98), ACM Press, New York, February 1998, pp. 211\u2013217","DOI":"10.1109\/DATE.1998.655859"},{"key":"10.1016\/S1383-7621(00)00034-5_BIB22","doi-asserted-by":"crossref","unstructured":"B. Lin, Software synthesis of process-based concurrent programs, in: Proceedings of Design Automation Conference (DAC'98), ACM Press, New York, June 1998, pp. 502\u2013505","DOI":"10.1145\/277044.277182"},{"key":"10.1016\/S1383-7621(00)00034-5_BIB23","doi-asserted-by":"crossref","unstructured":"O. Maler, A. Pnueli, J. Sifakis. On the synthesis of discrete controllers for timed systems, in: E. Mayr, C. Puech (Eds.), Proceedings of the 12th Annual Symposium on Theoretical Aspects of Computer Science (STACS'95), vol. 900, Lecture Notes in Computer Science, Springer, Berlin, March 1995, pp. 229\u2013242","DOI":"10.1007\/3-540-59042-0_76"},{"issue":"1","key":"10.1016\/S1383-7621(00)00034-5_BIB24","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/357195.357196","article-title":"On the construction of submodule specifications and communication protocols","volume":"5","author":"Merlin","year":"1983","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"10.1016\/S1383-7621(00)00034-5_BIB25","doi-asserted-by":"crossref","unstructured":"M. Sgroi, L. Lavagno, Y. Watanabe, A. Sangiovanni-Vincentelli, Synthesis of embedded software using free-choice petri nets, in: Proceedings of the Design Automation Conference (DAC'99). ACM Press, New York, June 1999","DOI":"10.1145\/309847.310073"},{"key":"10.1016\/S1383-7621(00)00034-5_BIB26","doi-asserted-by":"crossref","unstructured":"H. Wong-Toi, G. Hoffman, The control of dense real-time discrete event systems. Technical report STAN-CS-92-1411, Stanford University, 1992","DOI":"10.21236\/ADA325997"},{"key":"10.1016\/S1383-7621(00)00034-5_BIB27","unstructured":"X. Zhu, B. Lin, Compositional software synthesis of communicating processes. in: Proceedings of International Conference on Computer Design (ICCD'99), IEEE CS Press, October 1999, pp. 646\u2013651"}],"container-title":["Journal of Systems Architecture"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1383762100000345?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1383762100000345?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2024,12,4]],"date-time":"2024-12-04T03:49:57Z","timestamp":1733284197000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S1383762100000345"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000,12]]},"references-count":27,"journal-issue":{"issue":"15","published-print":{"date-parts":[[2000,12]]}},"alternative-id":["S1383762100000345"],"URL":"https:\/\/doi.org\/10.1016\/s1383-7621(00)00034-5","relation":{},"ISSN":["1383-7621"],"issn-type":[{"type":"print","value":"1383-7621"}],"subject":[],"published":{"date-parts":[[2000,12]]}}}