{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,26]],"date-time":"2025-10-26T14:41:24Z","timestamp":1761489684071,"version":"3.41.0"},"publisher-location":"Wiesbaden","reference-count":59,"publisher":"Springer Fachmedien Wiesbaden","isbn-type":[{"type":"print","value":"9783658099930"},{"type":"electronic","value":"9783658099947"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-658-09994-7_1","type":"book-chapter","created":{"date-parts":[[2015,6,5]],"date-time":"2015-06-05T07:56:17Z","timestamp":1433490977000},"page":"1-25","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Verification of Embedded Real-time Systems"],"prefix":"10.1007","author":[{"given":"Paula","family":"Herber","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sabine","family":"Glesner","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,6,6]]},"reference":[{"key":"1_CR1","unstructured":"Alur, R., Dill, D.L.: A Theory of Timed Automata. Theoretical Computer Science"},{"key":"1_CR2","doi-asserted-by":"crossref","unstructured":"126, 183-235 (1994)","DOI":"10.1016\/0301-0104(94)00019-0"},{"key":"1_CR3","unstructured":"ARM Ltd.: AMBA3 AHB-Lite Protocol Specification (2006)"},{"key":"1_CR4","doi-asserted-by":"crossref","unstructured":"Behjati, R., Sabouri, H., Razavi, N., Sirjani, M.: An effective approach for model checking systemc designs. In: Application of Concurrency to System Design (ACSD). pp.\u00a056\u201361 (2008)","DOI":"10.1109\/ACSD.2008.4574596"},{"key":"1_CR5","doi-asserted-by":"crossref","unstructured":"Behrmann, G., David, A., Larsen, K.G.: A Tutorial on UPPAAL. In: Formal Methods for the Design of Real-Time Systems. pp.\u00a0200-236. LNCS 3185, Springer (2004)","DOI":"10.1007\/978-3-540-30080-9_7"},{"key":"1_CR6","doi-asserted-by":"crossref","unstructured":"Bengtsson, J., Yi, W.: Timed automata: Semantics, algorithms and tools. In: Lecture Notes on Concurrency and Petri Nets. pp.\u00a087-124. LNCS 3098, Springer (2004)","DOI":"10.1007\/978-3-540-27755-2_3"},{"key":"1_CR7","doi-asserted-by":"crossref","unstructured":"Berthomieu, B., Diaz, M.: Modeling and verification of time dependent systems using time petri nets. IEEE Transactions on Software Engineering 17(3) (1991)","DOI":"10.1109\/32.75415"},{"issue":"14","key":"1_CR8","doi-asserted-by":"publisher","first-page":"2741","DOI":"10.1080\/00207540412331312688","volume":"42","author":"B. Berthomieu","year":"2004","unstructured":"Berthomieu, B., Ribet, P.O., Vernadat, F.: The tool tina construction of abstract state spaces for petri nets and time petri nets. International Journal of Production Research 42(14), 2741\u20132756 (2004)","journal-title":"International Journal of Production Research"},{"key":"1_CR9","doi-asserted-by":"crossref","unstructured":"Blanc, N., Kroening, D., Sharygina, N.: Scoot: A Tool for the Analysis of SystemC Models. In: International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS). LNCS, vol.\u00a04963, pp.\u00a0467\u2013470. Springer (2008)","DOI":"10.1007\/978-3-540-78800-3_36"},{"issue":"6","key":"1_CR10","doi-asserted-by":"publisher","first-page":"667","DOI":"10.1007\/s10766-005-8908-x","volume":"33","author":"F. Bruschi","year":"2005","unstructured":"Bruschi, F., Ferrandi, F., Sciuto, D.: A framework for the functional verification of SystemC models. Int. Journal on Parallel Programming 33(6), 667\u2013695 (2005)","journal-title":"Journal on Parallel Programming"},{"key":"1_CR11","doi-asserted-by":"crossref","unstructured":"Chen, M., Mishra, P., Kalita, D.: Towards RTL test generation from SystemC TLM specifications. In: IEEE International High Level Design Validation and Test Workshop. pp.\u00a091\u201396. IEEE Computer Society (2007)","DOI":"10.1109\/HLDVT.2007.4392793"},{"key":"1_CR12","unstructured":"Cimatti, A., Micheli, A., Narasamdya, I., Roveri, M.: Verifying SystemC: A software model checking approach. In: Formal Methods in Computer-Aided Design (FMCAD), 2010. pp.\u00a051\u201359. IEEE (2010)"},{"key":"1_CR13","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Griggio, A., Micheli, A., Narasamdya, I., Roveri, M.: Kratos \u2013 A Software Model Checker for SystemC. In: Computer Aided Verification, LNCS, vol.\u00a06806, pp.\u00a0310\u2013316. Springer (2011)","DOI":"10.1007\/978-3-642-22110-1_24"},{"issue":"5","key":"1_CR14","doi-asserted-by":"publisher","first-page":"774","DOI":"10.1109\/TCAD.2012.2232351","volume":"32","author":"A. Cimatti","year":"2013","unstructured":"Cimatti, A., Narasamdya, I., Roveri, M.: Software model checking systemc. IEEE Trans. on CAD of Integrated Circuits and Systems 32(5), 774\u2013787 (2013)","journal-title":"IEEE Trans. on CAD of Integrated Circuits and Systems"},{"key":"1_CR15","unstructured":"FZI Research Center for Information Technology: KaSCPar \u2013 Karlsruhe SystemC Parser Suite"},{"key":"1_CR16","doi-asserted-by":"crossref","unstructured":"Garavel, H., Helmstetter, C., Ponsini, O., Serwe, W.: Verification of an industrial SystemC\/TLM model using LOTOS and CADP. In: Formal Methods and Models for Co-Design (MEMOCODE). pp.\u00a046\u201355. IEEE (2009)","DOI":"10.1109\/MEMCOD.2009.5185377"},{"key":"1_CR17","doi-asserted-by":"crossref","unstructured":"Gibson-Robinson, T., Armstrong, P., Boulgakov, A., Roscoe, A.: Fdr3 a modern refinement checker for csp. In: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol.\u00a08413, pp.\u00a0187\u2013201. Springer (2014)","DOI":"10.1007\/978-3-642-54862-8_13"},{"key":"1_CR18","unstructured":"Groetker, T.: System Design with SystemC. Kluwer Academic Publishers (2002)"},{"key":"1_CR19","doi-asserted-by":"crossref","unstructured":"Gro\u00dfe, D., Drechsler, R.: Checkers for SystemC designs. In: Formal Methods and Models for Codesign. pp.\u00a0171\u2013178. IEEE Computer Society (2004)","DOI":"10.1109\/MEMCOD.2004.1459851"},{"key":"1_CR20","doi-asserted-by":"crossref","unstructured":"Gro\u00dfe, D., K\u00fchne, U., Drechsler, R.: HW\/SW Co-Verification of Embedded Systems using Bounded Model Checking. In: Great Lakes Symposium on VLSI. pp.\u00a043\u201348. ACM Press (2006)","DOI":"10.1109\/MTV.2005.12"},{"key":"1_CR21","doi-asserted-by":"crossref","unstructured":"Gro\u00dfe, D., Peraza, H., Klingauf, W., Drechsler, R.: Embedded Systems Specification and Design Languages, chap. Measuring the Quality of a SystemC Testbench by Using Code Coverage Techniques, pp.\u00a073\u201386. Springer (2008)","DOI":"10.1007\/978-1-4020-8297-9_6"},{"key":"1_CR22","doi-asserted-by":"crossref","unstructured":"Habibi, A., Moinudeen, H., Tahar, S.: Generating Finite State Machines from Sys- temC. In: Design, Automation and Test in Europe. pp.\u00a076\u201381. IEEE (2006)","DOI":"10.1109\/DATE.2006.243777"},{"key":"1_CR23","doi-asserted-by":"crossref","unstructured":"Habibi, A., Tahar, S.: An Approach for the Verification of SystemC Designs Using AsmL. In: Automated Technology for Verification and Analysis. pp.\u00a069-83. LNCS 3707, Springer (2005)","DOI":"10.1007\/11562948_8"},{"key":"1_CR24","doi-asserted-by":"crossref","unstructured":"Hansel, J., Rose, D., Herber, P., Glesner, S.: An evolutionary algorithm for the generation of timed test traces for embedded real-time systems. In: Intl. Conf. on Software Testing, Verification and Validation (ICST). pp.\u00a0170\u2013179. IEEE (2011)","DOI":"10.1109\/ICST.2011.37"},{"key":"1_CR25","doi-asserted-by":"crossref","unstructured":"Herber, P., Fellmuth, J., Glesner, S.: Model Checking SystemC Designs Using Timed Automata. In: International Conference on Hardware\/Software Codesign and System Synthesis (CODES+ISSS). pp.\u00a0131\u2013136. ACM press (2008)","DOI":"10.1145\/1450135.1450166"},{"key":"1_CR26","doi-asserted-by":"crossref","unstructured":"Herber, P., Friedemann, F., Glesner, S.: Combining Model Checking and Testing in a Continuous HW\/SW Co-Verification Process. In: Tests and Proofs. LNCS, vol.\u00a05668. Springer (2009)","DOI":"10.1007\/978-3-642-02949-3_10"},{"key":"1_CR27","doi-asserted-by":"crossref","unstructured":"Herber, P., Glesner, S.: A HW\/SW Co-Verification Framework for SystemC. ACM Transactions on Embedded Computing Systems (2013)","DOI":"10.1145\/2435227.2435257"},{"key":"1_CR28","doi-asserted-by":"crossref","unstructured":"Herber, P., Pockrandt, M., Glesner, S.: Automated Conformance Evaluation of SystemC Designs using Timed Automata. In: IEEE European Test Symposium (2010)","DOI":"10.1109\/ETSYM.2010.5512761"},{"key":"1_CR29","doi-asserted-by":"crossref","unstructured":"Herber, P., Pockrandt, M., Glesner, S.: Transforming SystemC Transaction Level Models into UPPAAL Timed Automata. In: Formal Methods and Models for Codesign (MEMOCODE). pp.\u00a0161\u2013170. IEEE Computer Society (2011)","DOI":"10.1109\/MEMCOD.2011.5970523"},{"key":"1_CR30","unstructured":"Hessel, A., Larsen, K.G., Mikucionis, M., Nielsen, B., Pettersson, P., Skou, A.: Formal Methods and Testing, chap. Testing Real-Time Systems Using UPPAAL. Springer (2008)"},{"key":"1_CR31","doi-asserted-by":"crossref","unstructured":"Hessel, A., Larsen, K.G., Nielsen, B., Petterson, P., Skou, A.: Time-optimal test cases for real-time systems. In: Proceedings of the 3rd International Workshop on Formal Approaches to Testing of Software (FATES). pp.\u00a0114-130. LNCS 2931, Springer (2003)","DOI":"10.1007\/978-3-540-24617-6_9"},{"key":"1_CR32","unstructured":"IEEE Standards Association: IEEE Std. 1666-2011, Open SystemC Language Reference Manual (2011)"},{"key":"1_CR33","doi-asserted-by":"crossref","unstructured":"Jaghoori, M.M., Movaghar, A., Sirjani, M.: Modere: The Model-checking Engine of Rebeca. In: ACM Symposium on Applied Computing. pp.\u00a01810-1815. SAC \u201906, ACM (2006)","DOI":"10.1145\/1141277.1141704"},{"key":"1_CR34","doi-asserted-by":"crossref","unstructured":"Junior, A.D., Cecilio da Silva, D.J.: Code-coverage Based Test Vector Generation for SystemC Designs. In: IEEE Computer Society Annual Symposium on VLSI. pp.\u00a0198\u2013206. IEEE (2007)","DOI":"10.1109\/ISVLSI.2007.31"},{"key":"1_CR35","doi-asserted-by":"crossref","unstructured":"Kalaji, A.S., Hierons, R.M., Swift, S.: Generating Feasible Transition Paths for Testing from an Extended Finite State Machine (EFSM). In: Intl. Conf. on Software Testing Verification and Validation. pp.\u00a0230\u2013239. IEEE (2009)","DOI":"10.1109\/ICST.2009.29"},{"key":"1_CR36","doi-asserted-by":"crossref","unstructured":"Karlsson, D., Eles, P., Peng, Z.: Formal verification of SystemC Designs using a Petri-Net based Representation. In: Design, Automation and Test in Europe (DATE). pp.\u00a01228\u20131233. IEEE Press (2006)","DOI":"10.1109\/DATE.2006.244076"},{"key":"1_CR37","doi-asserted-by":"crossref","unstructured":"Kirchsteiger, C.M., Trummer, C., Steger, C., Weiss, R., Pistauer, M.: Distributed Embedded Systems: Design, Middleware and Resources, chap. Specification-based Verification of Embedded Systems by Automated Test Case Generation, pp.\u00a035\u201344. Springer (2008)","DOI":"10.1007\/978-0-387-09661-2_4"},{"key":"1_CR38","doi-asserted-by":"crossref","unstructured":"Krichen, M., Tripakis, S.: Real-time testing with timed automata testers and coverage criteria. In: Joint conference on Formal Modelling and Analysis of Timed Systems and Formal Techniques in Real-Time and Fault Tolerant System (FORMATS- FTRTFT). pp.\u00a0134-151. LNCS 3253, Springer (2004)","DOI":"10.1007\/978-3-540-30206-3_11"},{"key":"1_CR39","doi-asserted-by":"crossref","unstructured":"Kroening, D., Sharygina, N.: Formal Verification of SystemC by Automatic Hard- ware\/Software Partitioning. In: MEMOCODE. pp.\u00a0101\u2013110. IEEE (2005)","DOI":"10.1109\/MEMCOD.2005.1487900"},{"key":"1_CR40","doi-asserted-by":"crossref","unstructured":"Larsen, K.G., Mikucionis, M., Nielsen, B.: Formal Approaches to Software Testing, chap. Online Testing of Real-time Systems Using UPPAAL, pp.\u00a079\u201394. Springer (2005)","DOI":"10.1007\/978-3-540-31848-4_6"},{"key":"1_CR41","doi-asserted-by":"crossref","unstructured":"Le, H.M., Gro\u00dfe, D., Herdt, V., Drechsler, R.: Verifying SystemC using an intermediate verification language and symbolic simulation. In: DAC. p.\u00a0116 (2013)","DOI":"10.1145\/2463209.2488877"},{"key":"1_CR42","doi-asserted-by":"crossref","unstructured":"Lefticaru, R., Ipate, F.: Automatic State-based Test Generation using Genetic Algorithms. In: International Symposium on Symbolic and Numeric Algorithms for Scientific Computing. pp.\u00a0188\u2013195. IEEE Computer Society (2007)","DOI":"10.1109\/SYNASC.2007.47"},{"key":"1_CR43","first-page":"145","volume":"1","author":"K.L. Man","year":"2005","unstructured":"Man, K.L.: An Overview of SystemCFL. In: Research in Microelectronics and Electronics. vol.\u00a01, pp.\u00a0145\u2013148 (2005)","journal-title":"Research in Microelectronics and Electronics"},{"key":"1_CR44","doi-asserted-by":"crossref","unstructured":"Mathaikutty, D.A., Ahuja, S., Dingankar, A., Shukla, S.: Model-driven test generation for system level validation. In: IEEE International High Level Design Validation and Test Workshop. pp.\u00a083\u201390. IEEE Computer Society (2007)","DOI":"10.1109\/HLDVT.2007.4392792"},{"key":"1_CR45","doi-asserted-by":"crossref","unstructured":"M\u00fcller, W., Ruf, J., Rosenstiel, W.: SystemC: Methodologies and Applications, chap. An ASM based SystemC Simulation Semantics, pp.\u00a097\u2013126. Kluwer Academic Publishers (2003)","DOI":"10.1007\/0-306-48735-7_4"},{"key":"1_CR46","doi-asserted-by":"crossref","unstructured":"Nielsen, B., Skou, A.: Automated test generation from timed automata. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). pp.\u00a0343-357. LNCS 2031, Springer (2001)","DOI":"10.1007\/3-540-45319-9_24"},{"issue":"3","key":"1_CR47","first-page":"1","volume":"2008","author":"H.D. Patel","year":"2008","unstructured":"Patel, H.D., Shukla, S.K.: Model-driven validation of SystemC designs. EURASIP Journal on Embedded Systems 2008(3), 1\u201314 (2008)","journal-title":"EURASIP Journal on Embedded Systems"},{"key":"1_CR48","doi-asserted-by":"crossref","unstructured":"Pockrandt, M., Herber, P., Glesner, S.: Model Checking a SystemC\/TLM Design of the AMBA AHB Protocol. In: IEEE\/ACM Symposium on Embedded Systems For Real-time Multimedia (ESTIMedia). pp.\u00a066\u201375. IEEE Computer Society (2011)","DOI":"10.1109\/ESTIMedia.2011.6088527"},{"key":"1_CR49","doi-asserted-by":"crossref","unstructured":"Pockrandt, M., Herber, P., Kl\u00fcs, V., Glesner, S.: Model Checking Memory-Related Properties of Hardware\/Software Co-Designs. In: Embedded Systems: Design, Analysis and Verification. Proceedings of the International Embedded Systems Symposium (IESS). Springer (2013)","DOI":"10.1007\/978-3-642-38853-8_9"},{"issue":"2","key":"1_CR50","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1145\/1880050.1880055","volume":"10","author":"N. Razavi","year":"2010","unstructured":"Razavi, N., Behjati, R., Sabouri, H., Khamespanah, E., Shali, A., Sirjani, M.: Sys- fier: Actor-based formal verification of SystemC. ACM Trans. Embedded Comput. Syst. 10(2), 19 (2010)","journal-title":"ACM Trans. Embedded Comput. Syst"},{"key":"1_CR51","unstructured":"Ruf, J., Hoffmann, D.W., Gerlach, J., Kropf, T., Rosenstiel, W., M\u00fcller, W.: The Simulation Semantics of SystemC. In: Design, Automation and Test in Europe. pp.\u00a064\u201370. IEEE Press (2001)"},{"key":"1_CR52","unstructured":"Schneider, S.: Concurrent and Real Time Systems: The CSP Approach. John Wiley & Sons, Inc. (1999)"},{"key":"1_CR53","doi-asserted-by":"crossref","unstructured":"da Silva, K.R.G., Melcher, E.U.K., Araujo, G., Pimenta, V.A.: An automatic testbench generation tool for a SystemC functional verification methodology. In: Symposium on Integrated circuits and system design. pp.\u00a066\u201370. ACM Press (2004)","DOI":"10.1145\/1016568.1016592"},{"key":"1_CR54","unstructured":"SystemC Verification Working Group \u2013 SCV: SystemC Verification Standard (2006)"},{"key":"1_CR55","unstructured":"Tracey, N.J.: A Search-based Automated Test-Data Generation Framework for Safety-Critical Software. Ph.D. thesis, University of York (2000)"},{"key":"1_CR56","doi-asserted-by":"crossref","unstructured":"Traulsen, C., Cornet, J., Moy, M., Maraninchi:, F.: A SystemC\/TLM semantics in Promela and its possible applications. In: 14th Workshop on Model Checking Software (SPIN \u201907). pp.\u00a0204-222. LNCS 4595, Springer (2007)","DOI":"10.1007\/978-3-540-73370-6_14"},{"key":"1_CR57","doi-asserted-by":"crossref","unstructured":"Veanes, M., Campbell, C., Grieskamp, W., Schulte, W., Tillmann, N., Nachmanson, L.: Model-Based Testing of Object-Oriented Reactive Systems with Spec Explorer. In: Formal Methods and Testing, LNCS, vol.\u00a04949, pp.\u00a039\u201376. Springer (2008)","DOI":"10.1007\/978-3-540-78917-8_2"},{"key":"1_CR58","doi-asserted-by":"crossref","unstructured":"de Vries, R.G., Tretmans, J.: On-the-fly conformance testing using SPIN. Software Tools for Technology Transfer 2(4), 382\u2013393 (2000)","DOI":"10.1007\/s100090050044"},{"key":"1_CR59","unstructured":"Wegener, J., Buhr, K., Pohlheim, H.: Automatic Test Data Generation For Structural Testing Of Embedded Software Systems By Evolutionary Testing. In: Proceedings of the Genetic and Evolutionary Computation Conference. pp.\u00a01233\u20131240. Morgan Kaufmann Publishers Inc. (2002)"}],"container-title":["Formal Modeling and Verification of Cyber-Physical Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-658-09994-7_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,28]],"date-time":"2025-05-28T10:34:59Z","timestamp":1748428499000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-658-09994-7_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783658099930","9783658099947"],"references-count":59,"URL":"https:\/\/doi.org\/10.1007\/978-3-658-09994-7_1","relation":{},"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"6 June 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}