{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,31]],"date-time":"2025-10-31T19:16:26Z","timestamp":1761938186692,"version":"build-2065373602"},"reference-count":77,"publisher":"Springer Science and Business Media LLC","issue":"6","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":["Int J Parallel Prog"],"published-print":{"date-parts":[[2005,12]]},"DOI":"10.1007\/s10766-005-8911-2","type":"journal-article","created":{"date-parts":[[2005,11,14]],"date-time":"2005-11-14T11:28:47Z","timestamp":1131967727000},"page":"585-611","source":"Crossref","is-referenced-by-count":9,"title":["Dynamic and Formal Verification of Embedded Systems: A Comparative Survey"],"prefix":"10.1007","volume":"33","author":[{"given":"Mirko","family":"Loghi","sequence":"first","affiliation":[]},{"given":"Tiziana","family":"Margaria","sequence":"additional","affiliation":[]},{"given":"Graziano","family":"Pravadelli","sequence":"additional","affiliation":[]},{"given":"Bernhard","family":"Steffen","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"1","key":"8911_CR1","doi-asserted-by":"crossref","first-page":"136","DOI":"10.1109\/2.976929","volume":"35","author":"W. Wolf","year":"January 2002","journal-title":"IEEE Computer."},{"issue":"2","key":"8911_CR2","doi-asserted-by":"crossref","first-page":"45","DOI":"10.1109\/54.679207","volume":"15","author":"R. Ernst","year":"April\u2013June 1998","journal-title":"IEEE Design and Test of Computers."},{"key":"8911_CR3","doi-asserted-by":"crossref","unstructured":"R. A. Bergamaschi and J. Cohn, The A to Z of SoCs, IEEE, pp. 791\u2013798 (2002)","DOI":"10.1145\/774572.774689"},{"key":"8911_CR4","unstructured":"S. M. Sze, Physics of Semiconductor Devices, John Wiley and Sons (1981)"},{"key":"8911_CR5","unstructured":"S. Hall, G. Hall, and J. McCall, High-Speed Digital System Design: A Handbook of Interconnect Theory and Design Practices, John Wiley and Sons (2000)"},{"key":"8911_CR6","doi-asserted-by":"crossref","unstructured":"L. Benini and M. Poncino, Ambient Intelligence: A Computational Platform Perspective, Ambient Intelligence: Impact on Embedded System Design, Kluwer Academic Publishers, pp. 31\u201350 (2003)","DOI":"10.1007\/0-306-48706-3_3"},{"key":"8911_CR7","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1109\/54.970421","volume":"18","author":"A. Sangiovanni-Vincentelli","year":"2001","journal-title":"IEEE Design and Test of Computers."},{"issue":"8","key":"8911_CR8","doi-asserted-by":"crossref","first-page":"1090","DOI":"10.1109\/5.533956","volume":"84","author":"D. Lee","year":"1996","journal-title":"Proceedings of the IEEE."},{"issue":"6","key":"8911_CR9","doi-asserted-by":"crossref","first-page":"311","DOI":"10.1049\/sej.1990.0034","volume":"5","author":"A. Valenzano","year":"1990","journal-title":"IEEE Software Engineering Journal."},{"key":"8911_CR10","unstructured":"E. Clarke, O. Grumberg, and D. Peled, Model Checking, MIT Press (2000)"},{"key":"8911_CR11","doi-asserted-by":"crossref","unstructured":"L. Cortes, P. Eles, and Z. Peng, Hierarchical Modeling and Verification of Embedded Systems, Proceedings of IEEE Euromicro Symposium on Digital System Design, pp. 63\u201370 (2001)","DOI":"10.1109\/DSD.2001.952119"},{"key":"8911_CR12","doi-asserted-by":"crossref","unstructured":"L. Gomes and J. P. Barros, On Structuring Mechanisms for Petri Nets based Systems Design, IEEE, pp. 431\u2013438 (2003)","DOI":"10.1109\/ETFA.2003.1248731"},{"key":"8911_CR13","doi-asserted-by":"crossref","unstructured":"R. Ernst and A. A. Jerraya, Embedded System Design with Multiple Languages, Proceedings of IEEE Conference on Asia and South Pacific Design Automation, pp. 391\u2013396 (2000)","DOI":"10.1145\/368434.368701"},{"key":"8911_CR14","unstructured":"Synopsys Inc., SystemC User\u2019s Guide, http:\/\/www.systemc.org"},{"key":"8911_CR15","unstructured":"J. Armstrong and F. Gray, VHDL Design Representation and Synthesis, Prentice Hall (2000)"},{"key":"8911_CR16","unstructured":"V. Sagdeo, The Complete Verilog Book, Kluwer Academic Publisher (1998)"},{"key":"8911_CR17","unstructured":"M. Breuer, M. Abramovici, and A. Friedman, Digital Systems Testing and Testable Design, IEEE Press (1990)"},{"key":"8911_CR18","doi-asserted-by":"crossref","unstructured":"D. Gajski, N. Dutt, S. Allen, C. Wu, and Y. Lin, High-Level Synthesis: Introduction to Chip and System Design, 1st edn., Kluwer Academic Publishers (1992)","DOI":"10.1007\/978-1-4615-3636-9"},{"key":"8911_CR19","unstructured":"J. Bergeron, Writing Testbenches: Functional Verification of HDL Models, Kluwer Academic Publishers, Norwell Massachusetts (2000)"},{"volume-title":"The Art of Software Testing","year":"1979","author":"G. Myers","key":"8911_CR20"},{"issue":"2","key":"8911_CR21","first-page":"155","volume":"4","author":"J. Buck","year":"1994","journal-title":"International Journal in Computer Simulation."},{"key":"8911_CR22","doi-asserted-by":"crossref","unstructured":"F. Balarin, M. Chiodo, P. Giusto, H. Hsieh, A. Jurecska, L Lavagno, C. Passerone, A. Sangiovanni-Vincentelli, E. Sentovich, K. Suzuki, and B. Tabbara, Hardware-Software Co-Design of Embedded Systems: The Polis Approach, Kluwer Academic Press (1997)","DOI":"10.1007\/978-1-4615-6127-9"},{"key":"8911_CR23","unstructured":"Synopsys Inc., Eaglei, http:\/\/www.synopsys.com\/products"},{"key":"8911_CR24","unstructured":"Mentor Graphics Inc., Seamless CVE, http:\/\/www.mentor.com\/seamless"},{"issue":"2","key":"8911_CR25","doi-asserted-by":"crossref","first-page":"16","DOI":"10.1109\/54.587736","volume":"14","author":"C. Liem","year":"1997","journal-title":"IEEE Design and Test of Computers."},{"issue":"2\/3","key":"8911_CR26","doi-asserted-by":"crossref","first-page":"199","DOI":"10.1023\/A:1008898525388","volume":"3","author":"C. Valderrama","year":"1998","journal-title":"Design Automation for Embedded Systems."},{"key":"8911_CR27","doi-asserted-by":"crossref","unstructured":"P. Coste, F. Hessel, P. L. Marrec, Z. Sugar, M. Romdhani, R Suescun, N. Zergainoh, and A. Jerraya, Multilanguage Design of Heterogeneous Systems, Proceedings of IEEE International Workshop on Hardware-Software Codesign, pp. 54\u201358 (1999)","DOI":"10.1145\/301177.301206"},{"issue":"4","key":"8911_CR28","doi-asserted-by":"crossref","first-page":"53","DOI":"10.1109\/MC.2003.1193229","volume":"36","author":"L. Benini","year":"2003","journal-title":"IEEE Computer."},{"key":"8911_CR29","doi-asserted-by":"crossref","unstructured":"J. Liu, M. Lajolo, and A. Sangiovanni-Vincentelli, Software Timing Analysis Using HW\/SW Co-Simulation and Instruction Set Simulator, Proceedings of IEEE International Workshop on Hardware\/Software Co-design, pp. 65\u201369 (1998)","DOI":"10.1145\/278241.278299"},{"key":"8911_CR30","doi-asserted-by":"crossref","unstructured":"L. Semeria and A. Ghosh, Methodology for Hardware\/Software Co-verification in C\/C++, Proceedings of IEEE Asian and South Pacific Design Automation Conference (ASP-DAC), pp 405\u2013408 (2000)","DOI":"10.1109\/ASPDAC.2000.835134"},{"key":"8911_CR31","doi-asserted-by":"crossref","unstructured":"K. Lahiri, A. Raghunathan, G. Lakshminarayana, and S. Dey, Communication Architecture Tuners: A Methodology for the Design of High-Performance Communication Architectures for System-on-Chips, Proceedings of ACM\/IEEE Design Automation Conference (DAC), pp. 513\u2013518 (2000)","DOI":"10.1145\/337292.337561"},{"key":"8911_CR32","doi-asserted-by":"crossref","unstructured":"F. Fummi, S. Martini, G. Perbellini, and M. Poncino, Native ISS-SystemC Integration for the Co-simulation of Multi-Processors SoC, Proceedings of IEEE Design Automation and Test in Europe, pp. 564\u2013569 (2004)","DOI":"10.1109\/DATE.2004.1268905"},{"key":"8911_CR33","doi-asserted-by":"crossref","unstructured":"I. Moussa, T. Grellier, and G. Nguyen, Exploring SW Performance Using SoC Transaction-level Modelling, Proceedings of IEEE Design Automation and Test in Europe, pp. 120\u2013125 (2003)","DOI":"10.1109\/DATE.2003.1253816"},{"key":"8911_CR34","unstructured":"GNU Project Web server, http:\/\/www.gnu.org\/software\/"},{"key":"8911_CR35","unstructured":"S. Yoo, I. Bacivarov, A. Bouchhima, Y. Paviot, and A. Jerraya, Building Fast and Accurate SW Simulation Models Based on Hardware Abstraction Layer and Simulation Environment Abstraction Layer, Proceedings of IEEE Design Automation and Test in Europe, pp 550\u2013555 (2003)"},{"key":"8911_CR36","doi-asserted-by":"crossref","unstructured":"I. Bacivarov, S. Yoo, and A. Jerraya, Timed HW-SW Cosimulation Using Native Execution of OS and Application SW, Proceedings of IEEE International High Level Design Validation and Test Workshop, pp. 51\u201356 (2002)","DOI":"10.1109\/HLDVT.2002.1224428"},{"key":"8911_CR37","doi-asserted-by":"crossref","unstructured":"L. Formaggio, F. Fummi, and G. Pravadelli, A Timing-Accurate HW\/SW Co-simulation of an ISS with SystemC, Proceedings of IEEE International Conference on Hardware\/Software Codesign and System Synthesis, pp. 152\u2013157 (2004)","DOI":"10.1145\/1016720.1016759"},{"key":"8911_CR38","unstructured":"ITUTS. ITUTS Recommendation Z.100: Specification and Description Language (SDL) (1988)"},{"key":"8911_CR39","unstructured":"ITUTS. ITUTS Recommendation Z.120: Message Sequence Chart (MSC) (1994)"},{"key":"8911_CR40","unstructured":"ITUTS. ITUTS Recommendation Z.120 Annex B: Algebraic semantics of Message Sequence Charts (1995)"},{"issue":"1","key":"8911_CR41","doi-asserted-by":"crossref","first-page":"68","DOI":"10.1007\/s100090050018","volume":"2","author":"M. Sighireanu","year":"1998","journal-title":"Journal on Software Tools for Technology Transfer."},{"key":"8911_CR42","unstructured":"E. Clarke, O. Grumberg, H. Hiraishi, D. L. S. Jha, K. McMillan, and L. Ness, Verfication of the Futurebus+Cache Coherence Protocol, Proceedings of International Symposium on Computer Hardware Description Languages and their Applications (1993)"},{"issue":"3","key":"8911_CR43","doi-asserted-by":"crossref","first-page":"181","DOI":"10.1109\/32.489079","volume":"22","author":"R. Alur","year":"1996","journal-title":"IEEE Transactions on Software Engineering."},{"key":"8911_CR44","first-page":"64","volume":"1","author":"K.G. Larsen","year":"1997","journal-title":"Special Section on Timed and Hybrid Systems."},{"key":"8911_CR45","doi-asserted-by":"crossref","unstructured":"J. -P. Katoen, H. Bohnenkamp, H. Hermanns, and J. Klaren, Embedded Software Analysis with MOTOR, Formal Methods for the Design of Computer, Communication and Software Systems: Real Time (2004)","DOI":"10.1007\/978-3-540-30080-9_9"},{"key":"8911_CR46","unstructured":"R. Milner, Communication and Concurrency, Prentice Hall (1989)"},{"key":"8911_CR47","doi-asserted-by":"crossref","unstructured":"C. Hoare, Communicating Sequential Processes, Prentice Hall (1986)","DOI":"10.1007\/978-3-642-82921-5_4"},{"key":"8911_CR48","doi-asserted-by":"crossref","unstructured":"C. Tofts, A Synchronous Calculus of Relative Frequency, CONCUR, LNCS, Vol. 458, pp. 467\u2013480 (1990)","DOI":"10.1007\/BFb0039078"},{"key":"8911_CR49","unstructured":"ISO Standard 8807: LOTOS \u2013 A Formal Description Technique based on the Temporal Ordering of Observational Behaviour (1989)"},{"key":"8911_CR50","unstructured":"S. F\u00f6rster, A. Windisch, M. Fischer, D. Monjau, and B. Balser, Process Algebraic Specification, Refinement, and Verification of Embedded Systems, Proceedings of ECSI Forum on Specification and Design Languages, pp. 525\u2013535 (2003)"},{"issue":"1","key":"8911_CR51","doi-asserted-by":"crossref","first-page":"64","DOI":"10.1109\/JPROC.2002.805826","volume":"91","author":"A. Benveniste","year":"2003","journal-title":"Proceedings of the IEEE."},{"key":"8911_CR52","doi-asserted-by":"crossref","unstructured":"N. Halbwachs, Synchronous Programming of Reactive Systems, Kluwer Academic Publisher (1993)","DOI":"10.1007\/978-1-4757-2231-4"},{"key":"8911_CR53","doi-asserted-by":"crossref","unstructured":"D. Harel, Statecharts: A Visual Formalism for Complex Systems, Science of Computing Programming, pp. 231\u2013274 (1987)","DOI":"10.1016\/0167-6423(87)90035-9"},{"key":"8911_CR54","doi-asserted-by":"crossref","unstructured":"F. Maraninchi, Argonaute: Graphical Description, Semantics and Verification of Reactive Systems by using a Process Algebra, Proceedings of Int. Workshop on Automatic Verification Methods for Finite State Systems, pp. 38\u201353 (1990)","DOI":"10.1007\/3-540-52148-8_4"},{"key":"8911_CR55","unstructured":"C. Andr\u00e8, SyncCharts: A Visual Representation of Reactive Behaviors, Technical Report TR-92-52, Universit\u00e8 de Nice, Sophia-Antipolis (1995)"},{"key":"8911_CR56","doi-asserted-by":"crossref","unstructured":"W. Damm and D. Harel, LSC: Breathing Life into Message Sequence Charts, Formal Methods in System Design, pp. 45\u201380 (2001)","DOI":"10.1023\/A:1011227529550"},{"key":"8911_CR57","doi-asserted-by":"crossref","unstructured":"N. Halbwachs, P. Caspi, and D. Pilaud, The Synchronous Programming Language Lustre, Proceedings of IEEE, pp. 1305\u20131320 (1991)","DOI":"10.1109\/5.97300"},{"issue":"5","key":"8911_CR58","doi-asserted-by":"crossref","first-page":"525","DOI":"10.1109\/9.53519","volume":"35","author":"A. Benveniste","year":"1990","journal-title":"IEEE Transactions on Automatic Control."},{"key":"8911_CR59","unstructured":"Esterel Technologies: The SCADE Suite for Safety-Critical Software Development, http:\/\/www.esterel-technologies.com\/v2\/scadeSuiteForSafetyCriticalSoftwareDevelopment"},{"key":"8911_CR60","unstructured":"G. Berry, The Foundations of Esterel, MIT Press (1988)"},{"key":"8911_CR61","unstructured":"G. Berry, The Constructive Semantics of Pure Esterel, http:\/\/www.esterel-technologies.com"},{"key":"8911_CR62","doi-asserted-by":"crossref","first-page":"64","DOI":"10.1109\/MC.2004.172","volume":"37","author":"D. Harel","year":"2004","journal-title":"IEEE Computer."},{"key":"8911_CR63","unstructured":"C. Dumoulin, J. -L. Dekeyser, B. Kokoszko, S. Pulon, and G Cristau, Interoperability between Design and Simulation Tools using Model Transformation Techniques, Proceedings of ECSI Forum on Specification and Design Languages (2003)"},{"key":"8911_CR64","unstructured":"W. M\u00fcller and G. Martin, DAC 2004 Workshop on UML for SoC Design, Proceedings of Workshop on Specification and Validation of UML Models for Real-Time Embedded Systems (2004)"},{"key":"8911_CR65","unstructured":"W. Tan, P. Thiagarajan, W. Wong, Y. Zhu, and S. Pilakkat, Synthesizable SystemC Code from UML Models, DAC Workshop on UML for SoC Design (2004)"},{"key":"8911_CR66","unstructured":"P. Boulet, A. Cuccuru, J.-L. Dekeyser, C. Dumoulin, P. Marquet, M. Samyn, R. D. Simone, G. Siegel, and T. Saunier, MDA for SoC Design: UML To SystemC Experiment, DAC Workshop on UML for SoC Design (2004)"},{"key":"8911_CR67","unstructured":"The Omega Project, http:\/\/www-omega.imag.fr"},{"key":"8911_CR68","unstructured":"M. Bozga, J. Fernandez, L. Ghirvu, S. Graf, J. Krimm, and L Mounier, An Intermediate Representation and Validation Environment for Timed Asynchronous Systems, Formal Methods\u201999, LNCS, Vol. 1708, pp. 307\u2013327 (1999)"},{"key":"8911_CR69","doi-asserted-by":"crossref","unstructured":"I. Ober, S. Graf, and I. Ober, Model Checking of UML Models via a Mapping to Communicating Extended Timed Automata, SPIN Workshop on Model Checking of Software (2004)","DOI":"10.1007\/978-3-540-24732-6_9"},{"key":"8911_CR70","doi-asserted-by":"crossref","unstructured":"S. Graf and J. Hooman, Correct Development of Embedded Systems, Proceedings of European Workshop of Software Architecture (2004)","DOI":"10.1007\/978-3-540-24769-2_21"},{"key":"8911_CR71","unstructured":"M. Bozga, S. Graf, and L. Mounier, IF-2.0: A Validation Environment for Component-based Real-Time Systems, Proceedings of International Conference on computer Aided Verification, LNCS, Vol. 2404, pp. 343\u2013348 (2002)"},{"key":"8911_CR72","doi-asserted-by":"crossref","unstructured":"M. Bozga, S. Graf, and L. Mounier, Automated Validation of Distributed Software Using the IF Environment, Proceedings of IEEE International Symposium on Network Computing and Applications, pp. 268\u2013275 (2001)","DOI":"10.1109\/NCA.2001.962542"},{"key":"8911_CR73","doi-asserted-by":"crossref","unstructured":"D. Harel, H. Kugler, R. Marelly, and A. Pnueli, Smart Play-out, Proceedings of ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications (2003)","DOI":"10.1145\/949344.949353"},{"key":"8911_CR74","unstructured":"T. Bienmller, W. Damm, and H. Wittke, The STATEMATE Verification Environment Making it Real, Proceedings of International Conference on computer Aided Verification, LNCS, Vol. 1855, pp. 561\u2013567 (2000)"},{"key":"8911_CR75","unstructured":"N. Shankar, S. Owre, and J. Rushby, The PVS Proof Checker: A Reference Manual, Technical report, Computer Science Laboratory, SRI International (1993)"},{"key":"8911_CR76","unstructured":"M. Kyas and F. de Boer, On message specification in OCL, Compositional Verification in UML, Workshop associated with UML 2003 (2003)"},{"key":"8911_CR77","unstructured":"M. Zwaag and J. Hooman, A Semantics of Communicating Reactive Objects with Timing, Proceedings of Workshop on Specification and Validation of UML models for Real-Time Embedded Systems (2003)"}],"container-title":["International Journal of Parallel Programming"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10766-005-8911-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10766-005-8911-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10766-005-8911-2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,5]],"date-time":"2025-01-05T13:33:08Z","timestamp":1736083988000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10766-005-8911-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005,12]]},"references-count":77,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2005,12]]}},"alternative-id":["8911"],"URL":"https:\/\/doi.org\/10.1007\/s10766-005-8911-2","relation":{},"ISSN":["0885-7458","1573-7640"],"issn-type":[{"type":"print","value":"0885-7458"},{"type":"electronic","value":"1573-7640"}],"subject":[],"published":{"date-parts":[[2005,12]]}}}