{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,26]],"date-time":"2026-02-26T11:55:01Z","timestamp":1772106901612,"version":"3.50.1"},"reference-count":15,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2006,1,25]],"date-time":"2006-01-25T00:00:00Z","timestamp":1138147200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int J Parallel Prog"],"published-print":{"date-parts":[[2006,3]]},"DOI":"10.1007\/s10766-005-0002-x","type":"journal-article","created":{"date-parts":[[2006,1,25]],"date-time":"2006-01-25T20:08:09Z","timestamp":1138219689000},"page":"3-27","source":"Crossref","is-referenced-by-count":8,"title":["Verification Approach of Metropolis Design Framework for Embedded Systems"],"prefix":"10.1007","volume":"34","author":[{"given":"Xi","family":"Chen","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Harry","family":"Hsieh","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Felice","family":"Balarin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2006,1,25]]},"reference":[{"issue":"12","key":"2_CR1","doi-asserted-by":"crossref","first-page":"1523","DOI":"10.1109\/43.898830","volume":"19","author":"K. Keutzer","year":"December 2000","unstructured":"Keutzer K., Malik S., Newton A.R., Rabaey J., Sangiovanni-Vincentelli A. (December 2000). System Level Design: Orthogonalization of Concerns and Platform-based Design. IEEE Trans, Computer-Aided Design. 19(12):1523\u20131543","journal-title":"IEEE Trans, Computer-Aided Design"},{"issue":"4","key":"2_CR2","doi-asserted-by":"crossref","first-page":"45","DOI":"10.1109\/MC.2003.1193228","volume":"36","author":"F. Balarin","year":"April 2003","unstructured":"Balarin F., Watanabe Y., Hsieh H., Lavagno L., Passerone C., Sangiovanni-Vincentelli A. (April 2003). Metropolis: An Integrated Electronic System Design Environment. IEEE Comput 36(4):45\u201352","journal-title":"IEEE Comput"},{"key":"2_CR3","unstructured":"P. Godefroid and G. J. Holzmann, On the Verification of Temporal Properties, Proceedings of IFIP\/WG6.1 Symposium on Protocols Specification, Testing, and Verification (June 1993)."},{"key":"2_CR4","doi-asserted-by":"crossref","unstructured":"F. Balarin, Y. Watanabe, J. Burch, L. Lavagno, R. Passerone, and A. Sangiovanni-Vincentelli, Constraints Specification at Higher Levels of Abstraction, Proceedings of International Workshop on High Level Design Validation and Test (November 2001).","DOI":"10.1109\/HLDVT.2001.972819"},{"issue":"5","key":"2_CR5","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G.J. Holzmann","year":"May 1997","unstructured":"Holzmann G.J. (May 1997). The Model Checker Spin. IEEE Trans. Software Eng. 23(5):279\u2013258","journal-title":"IEEE Trans. Software Eng."},{"key":"2_CR6","doi-asserted-by":"crossref","unstructured":"F. Balarin, L. Lavagno, C. Passerone, A. Sangiovanni-Vincentelli, M. Sgroi, and Y. Watanabe, Modeling and Designing Heterogeneous Systems, Technical Report 2001\/01 Cadence Berkeley Laboratories (November 2001).","DOI":"10.1007\/3-540-36190-1_7"},{"key":"2_CR7","doi-asserted-by":"crossref","unstructured":"X. Chen, H. Hsieh, F. Balarin, and Y. Watanabe, Verifying LOC BasedFunctional and Performance Constraints, Proceedings of International Workshop on High Level Design Validation and Test (November 2003).","DOI":"10.1109\/HLDVT.2003.1252479"},{"key":"2_CR8","doi-asserted-by":"crossref","unstructured":"Z. Manna and A. Pnueli, The Temporal Logic of Reactive and Concurrent Systems: Specification, Springer-Verlag (1992).","DOI":"10.1007\/978-1-4612-0931-7"},{"issue":"8","key":"2_CR9","doi-asserted-by":"crossref","first-page":"1243","DOI":"10.1109\/TCAD.2004.831575","volume":"23","author":"X. Chen","year":"August 2004","unstructured":"Chen X., Hsieh H., Balarin F., Watanabe Y. (August 2004). Logic of Constraints: A Quantitative Performance and Functional Constraint Formalism. IEEE Trans Computer-Aided Design Integrated Circuits. 23(8):1243\u20131255","journal-title":"IEEE Trans Computer-Aided Design Integrated Circuits."},{"key":"2_CR10","doi-asserted-by":"crossref","unstructured":"E. d. Kock, G. Essink, W. Smits, P. v. d. Wolf, J. Brunel, W. Kruijtzer, P. Lieverse, and K. Vissers, YAPI: Application Modeling for Signal Processing Systems, Proceedings of the 37 th Design Automation Conference, (June 2000).","DOI":"10.1145\/337292.337511"},{"key":"2_CR11","unstructured":"G. Kahn, The Semantics of a Simple Language for Parallel Programming, Proceedings of IFIP Congress, North Holland Publishing Company pp. 471\u2013475 (1974)."},{"key":"2_CR12","doi-asserted-by":"crossref","unstructured":"J. Brunel, E. A. de Kock, W. M. Kruijtzer, H. J. H. N. Kenter, and W. J. M. Smits, Communication Refinement In Video Systems on Chip, Proceedings of the 7th International Workshop on Hardware\/Software Codesign, pp. 142\u2013146 (1999).","DOI":"10.1145\/301177.301511"},{"key":"2_CR13","doi-asserted-by":"crossref","unstructured":"O. Gangwal, A. Nieuwland, and P. Lippens, A Scalable and Flexible Data Synchronization Scheme for Embedded HW-SW Shared-Memory Systems, Proceedings of International Symposium on System Synthesis (October 2001).","DOI":"10.1145\/500001.500003"},{"key":"2_CR14","unstructured":"C. Eisner and D. Fisman, Sugar 2.0 Proposal Presented to the Accellera Formal Verification Technical Committee (March 2002)."},{"key":"2_CR15","volume-title":"FoCs-Automatic Generation of Simulation Checkers from Formal Specifications","author":"Y. Abarbanel","year":"2003","unstructured":"Abarbanel Y., Beer I., Gluhovsky L., Keidar S., Wolfsthal Y. (2003). FoCs-Automatic Generation of Simulation Checkers from Formal Specifications, Technical Report, IBM Haifa Research Laboratory, Israel"}],"container-title":["International Journal of Parallel Programming"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10766-005-0002-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10766-005-0002-x\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10766-005-0002-x","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,30]],"date-time":"2019-05-30T23:59:24Z","timestamp":1559260764000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10766-005-0002-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,1,25]]},"references-count":15,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2006,3]]}},"alternative-id":["2"],"URL":"https:\/\/doi.org\/10.1007\/s10766-005-0002-x","relation":{},"ISSN":["0885-7458","1573-7640"],"issn-type":[{"value":"0885-7458","type":"print"},{"value":"1573-7640","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006,1,25]]}}}