{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,16]],"date-time":"2026-10-16T09:48:08Z","timestamp":1792144088835,"version":"4.4.0"},"publisher-location":"Dordrecht","reference-count":103,"publisher":"Springer Netherlands","isbn-type":[{"value":"9789401772662","type":"print"},{"value":"9789401772679","type":"electronic"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-94-017-7267-9_23","type":"book-chapter","created":{"date-parts":[[2017,9,26]],"date-time":"2017-09-26T09:54:06Z","timestamp":1506419646000},"page":"683-720","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Semiformal Assertion-Based Verification of Hardware\/Software Systems in a Model-Driven Design Framework"],"prefix":"10.1007","author":[{"given":"Graziano","family":"Pravadelli","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Davide","family":"Quaglia","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Sara","family":"Vinco","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Franco","family":"Fummi","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2017,9,27]]},"reference":[{"key":"23_CR1","unstructured":"3S Software (2012) CoDeSys. http:\/\/www.3s-software.com"},{"key":"23_CR2","doi-asserted-by":"crossref","unstructured":"Abarbanel Y, Beer I, Gluhovsky L, Keidar S, Wolfsthal Y (2000) FoCs: automatic generation of simulation checkers from formal specifications. In: Proceedings of international conference on computer aided verification (CAV), pp\u00a0538\u2013542","DOI":"10.1007\/10722167_40"},{"key":"23_CR3","unstructured":"Aerospace Valley (2012) TOPCASED project. http:\/\/www.topcased.org"},{"key":"23_CR4","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1007\/978-0-85729-277-3_7","volume-title":"Specification of software systems, texts in computer science","author":"V Alagar","year":"2011","unstructured":"Alagar V, Periyasamy K (2011) Extended finite state machine. In: Specification of software systems, texts in computer science. Springer, London, pp\u00a0105\u2013128. DOI 10.1007\/978-0-85729-277-3_7"},{"key":"23_CR5","first-page":"341","volume-title":"Mutation of Java objects","author":"RT Alexander","year":"2002","unstructured":"Alexander RT, Bieman JM, Ghosh S, Bixia J (2002) Mutation of Java objects. In: Proceedings of IEEE ISSRE, pp\u00a0341\u2013351"},{"issue":"2","key":"23_CR6","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R Alur","year":"1994","unstructured":"Alur R, Dill DL (1994) A theory of timed automata. Theoret Comput Sci 126(2):183\u2013235","journal-title":"Theoret Comput Sci"},{"key":"23_CR7","doi-asserted-by":"publisher","first-page":"368","DOI":"10.1007\/978-3-540-45069-6_35","volume-title":"International conference on computer aided verification","author":"R Armoni","year":"2003","unstructured":"Armoni R, Fix L, Flaisher A, Grumberg O, Piterman N, Tiemeyer A, Vardi M (2003) Enhanced vacuity detection in linear temporal logic (CAV). In: International conference on computer aided verification, vol\u00a02725. Springer, Berlin\/Heidelberg, pp\u00a0368\u2013380"},{"key":"23_CR8","unstructured":"Atego (2012) ARTiSAN. http:\/\/www.atego.com\/products\/artisan-studio"},{"key":"23_CR9","first-page":"50","volume-title":"Specification of timed EFSM fault models in SDL","author":"SS Batth","year":"2007","unstructured":"Batth SS, Vieira ER, Cavalli A, Umit Uyar M (2007) Specification of timed EFSM fault models in SDL. In: Proceedings of FORTE, pp\u00a050\u201365"},{"key":"23_CR10","doi-asserted-by":"crossref","unstructured":"Beer I, Ben-David S, Eisner U, Rodeh Y (1997) Efficient detection of vacuity in ACTL formulas. In: International conference on computer aided verification (CAV), vol\u00a01254, pp\u00a0279\u2013290","DOI":"10.1007\/3-540-63166-6_28"},{"issue":"2","key":"23_CR11","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1023\/A:1008779610539","volume":"18","author":"I Beer","year":"2001","unstructured":"Beer I, Ben-David S, Eisner C, Rodeh Y (2001) Efficient detection of vacuity in temporal model checking. Form Methods Syst Des 18(2):141\u2013163","journal-title":"Form Methods Syst Des"},{"key":"23_CR12","first-page":"10","volume-title":"Basic operations for generating behavioral mutants","author":"F Belli","year":"2006","unstructured":"Belli F, Budnik CJ, Wong WE (2006) Basic operations for generating behavioral mutants. In: Proceedings of IEEE ISSRE, pp\u00a010\u201318"},{"key":"23_CR13","first-page":"81","volume-title":"Mutation operators for specifications","author":"P Black","year":"2000","unstructured":"Black P, Okun V, Yesha Y (2000) Mutation operators for specifications. In: Proceedings of IEEE ASE, pp\u00a081\u201388"},{"issue":"5","key":"23_CR14","doi-asserted-by":"publisher","first-page":"1248","DOI":"10.1109\/TC.2012.301","volume":"63","author":"N Bombieri","year":"2014","unstructured":"Bombieri N, Fummi F, Guarnieri V, Pravadelli G (2014) Testbench qualification of systemc TLM protocols through mutation analysis. IEEE Trans Comput 63(5):1248\u20131261","journal-title":"IEEE Trans Comput"},{"key":"23_CR15","doi-asserted-by":"crossref","unstructured":"Bombieri N, Fummi F, Pravadelli G, Hampton M, Letombe F (2009) Functional qualification of TLM verification. In: Design, automation test in Europe conference exhibition, DATE\u201909, pp\u00a0190\u2013195. DOI 10.1109\/DATE.2009.5090656","DOI":"10.1109\/DATE.2009.5090656"},{"key":"23_CR16","unstructured":"Borrione D, Liu M, Morin-Allory K, Ostier P, Fesquet L (2005) On-line assertion-based verification with proven correct monitors. In: Proceedings of international conference on information and communications technology (ICICT), pp\u00a0125\u2013143"},{"key":"23_CR17","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1297666.1297670","volume":"13","author":"M Boul\u00e9","year":"2008","unstructured":"Boul\u00e9 M, Zilic Z (2008) Automata-based assertion-checker synthesis of PSL properties. ACM Trans Des Autom Electron Syst 13:1\u201321. http:\/\/doi.acm.org\/10.1145\/1297666.1297670","journal-title":"ACM Trans Des Autom Electron Syst"},{"issue":"1","key":"23_CR18","doi-asserted-by":"publisher","first-page":"135","DOI":"10.5381\/jot.2009.8.1.a1","volume":"8","author":"F Boutekkouk","year":"2009","unstructured":"Boutekkouk F, Benmohammed M, Bilavarn S, Auguin M et\u00a0al (2009) UML 2.0 profiles for embedded systems and systems on a chip (SoCs). J Object Technol 8(1):135\u2013157. DOI 10.5381\/jot.2009.8.1.a1","journal-title":"J Object Technol"},{"key":"23_CR19","first-page":"4","volume-title":"ExMan: a generic and customizable framework for experimental mutation analysis","author":"JS Bradbury","year":"2006","unstructured":"Bradbury JS, Cordy JR, Dingel J (2006) ExMan: a generic and customizable framework for experimental mutation analysis. In: Proceedings of IEEE ISSRE, pp\u00a04\u20139"},{"key":"23_CR20","doi-asserted-by":"crossref","unstructured":"Bradbury JS, Cordy JR, Dingel J (2006) Mutation operators for concurrent Java (J2SE 5.0). In: Proceedings of IEEE ISSRE, pp\u00a011\u201311","DOI":"10.1109\/MUTATION.2006.10"},{"key":"23_CR21","first-page":"221","volume-title":"On the use of a high-level fault model to analyze logical consequence of properties","author":"S Brait","year":"2005","unstructured":"Brait S, Fummi F, Pravadelli G (2005) On the use of a high-level fault model to analyze logical consequence of properties. In: Proceedings of ACM\/IEEE international conference on formal methods and models for co-design, MEMOCODE, pp\u00a0221\u2013230"},{"key":"23_CR22","unstructured":"Cadar C, Dunbar D, Engler D (2008) KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs. In: Proceedings of USENIX symposium on operating systems design and implementation (OSDI)"},{"key":"23_CR23","first-page":"322","volume-title":"EXE: a system for automatically generating inputs of death using symbolic execution","author":"C Cadar","year":"2006","unstructured":"Cadar C, Ganesh V, Pawlowski PM, Dill DL, Engler DR (2006) EXE: a system for automatically generating inputs of death using symbolic execution. In: ACM conference on computer and communications security, pp 322\u2013335"},{"key":"23_CR24","unstructured":"Cadence (2012) Assertion-based verification. http:\/\/www.cadence.com\/products\/fv\/pages\/abv_flow.aspx"},{"key":"23_CR25","doi-asserted-by":"crossref","unstructured":"Cheng KT, Jou JY (1990) A single-state-transition fault model for sequential machines. In: IEEE ICCAD\u201990, pp\u00a0226\u2013229","DOI":"10.1109\/ICCAD.1990.129887"},{"key":"23_CR26","doi-asserted-by":"crossref","unstructured":"Cheung P, Forin A (2007) A C-language binding for PSL. In: Proceedings of international conference on embedded software and systems (ICESS). Springer, pp\u00a0584\u2013591","DOI":"10.1007\/978-3-540-72685-2_54"},{"key":"23_CR27","first-page":"66","volume-title":"A practical approach to coverage in model checking","author":"H Chockler","year":"2001","unstructured":"Chockler H, Kupferman O, Kurshan R, Vardi M (2001) A practical approach to coverage in model checking. In: Proceedings computer aided and verification, pp\u00a066\u201378"},{"key":"23_CR28","doi-asserted-by":"publisher","first-page":"373","DOI":"10.1007\/s10009-004-0175-4","volume":"8","author":"H Chockler","year":"2006","unstructured":"Chockler H, Kupferman O, Vardi M (2006) Coverage metrics for formal verification. Int J Softw Tools Technol Transfer (STTT) 8:373\u2013386","journal-title":"Int J Softw Tools Technol Transfer (STTT)"},{"key":"23_CR29","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1007\/s10703-006-0001-6","volume":"28","author":"H Chockler","year":"2006","unstructured":"Chockler H, Kupferman O, Vardi M (2006) Coverage metrics for temporal logic model checking. Formal Methods Syst Des 28:189\u2013212","journal-title":"Formal Methods Syst Des"},{"key":"23_CR30","first-page":"189","volume-title":"Easier and more informative vacuity checks","author":"H Chockler","year":"2007","unstructured":"Chockler H, Strichman O (2007) Easier and more informative vacuity checks. In: Proceedings ACM\/IEEE international conference on formal methods and models for codesign, pp\u00a0189\u2013198"},{"key":"23_CR31","doi-asserted-by":"crossref","unstructured":"Choi BJ, DeMillo RA, Krauser EW, Martin RJ, Mathur AP, Pan AJOH, Spafford EH (1989) The Mothra tool set (software testing). In: Proceedings of IEEE HICSS, vol\u00a02, pp\u00a0275\u2013284","DOI":"10.1109\/HICSS.1989.48002"},{"issue":"3","key":"23_CR32","doi-asserted-by":"publisher","first-page":"178","DOI":"10.1109\/TSE.1978.231496","volume":"4","author":"T Chow","year":"1978","unstructured":"Chow T (1978) Testing software design modeled by finite state machines. IEEE Trans Softw Eng 4(3):178\u2013187","journal-title":"IEEE Trans Softw Eng"},{"key":"23_CR33","doi-asserted-by":"crossref","unstructured":"Dahan A, Geist D, Gluhovsky L, Pidan D, Shapir G, Wolfsthal Y, Benalycherif L, Kamidem R, Lahbib Y (2005) Combining system level modeling with assertion-based verification. In: Proceedings of international symposium on quality of electronic design (ISQED), pp\u00a0310\u2013315","DOI":"10.1109\/ISQED.2005.32"},{"key":"23_CR34","doi-asserted-by":"crossref","unstructured":"Das S, Mohanty R, Dasgupta P, Chakrabarti P (2006) Synthesis of system verilog assertions. In: Proceedings of design, automation & test in Europe conference & exhibition (DATE), vol\u00a02, pp\u00a01\u20136","DOI":"10.1109\/DATE.2006.243776"},{"issue":"2","key":"23_CR35","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1007\/s10009-005-0206-9","volume":"8","author":"R De Simone","year":"2006","unstructured":"De\u00a0Simone R, Andr\u00e9 C (2006) Towards a \u201csynchronous reactive\u201d UML profile? Int J Softw Tools Technol Transfer 8(2):146\u2013155","journal-title":"Int J Softw Tools Technol Transfer"},{"key":"23_CR36","unstructured":"Delamaro ME, Maldonado JC (1996) Proteum \u2013 a tool for the assessment of test adequacy for C programs. In: PCS\u201996, pp\u00a079\u201395"},{"issue":"4","key":"23_CR37","doi-asserted-by":"publisher","first-page":"34","DOI":"10.1109\/C-M.1978.218136","volume":"11","author":"RA DeMillo","year":"1978","unstructured":"DeMillo RA, Lipton RJ, Sayward FG (1978) Hints on test data selection: help for the practicing programmer. IEEE Comput 11(4):34\u201341","journal-title":"IEEE Comput"},{"issue":"8","key":"23_CR38","doi-asserted-by":"publisher","first-page":"2013","DOI":"10.1016\/j.jss.2012.08.061","volume":"86","author":"G Di Guglielmo","year":"2013","unstructured":"Di\u00a0Guglielmo G, Di\u00a0Guglielmo L, Foltinek A, Fujita M, Fummi F, Marconcini C, Pravadelli G (2013) On the integration of model-driven design and dynamic assertion-based verification for embedded software. J Syst Softw 86(8):2013\u20132033. DOI 10.1016\/j.jss.2012.08.061","journal-title":"J Syst Softw"},{"key":"23_CR39","first-page":"28","volume-title":"The role of mutation analysis for property qualification","author":"L Di Guglielmo","year":"2009","unstructured":"Di\u00a0Guglielmo L, Fummi F, Pravadelli G (2009) The role of mutation analysis for property qualification. In: IEEE\/ACM international conference on formal methods and models for co-design, MEMOCODE, pp\u00a028\u201335"},{"key":"23_CR40","doi-asserted-by":"crossref","unstructured":"Di\u00a0Guglielmo G, Fummi F, Pravadelli G, Soffia S, Roveri M (2010) Semi-formal functional verification by EFSM traversing via NuSMV. In: Proceedings of IEEE international high level design validation and test workshop (HLDVT), pp\u00a058\u201365","DOI":"10.1109\/HLDVT.2010.5496660"},{"key":"23_CR41","doi-asserted-by":"crossref","unstructured":"Di\u00a0Guglielmo L, Fummi F, Orlandi N, Pravadelli G (2010) DDPSL: an easy way of defining properties. In: 2010 IEEE international conference on computer design (ICCD), pp\u00a0468\u2013473","DOI":"10.1109\/ICCD.2010.5647654"},{"key":"23_CR42","doi-asserted-by":"crossref","unstructured":"Di\u00a0Guglielmo L, Fummi F, Pravadelli G (2010) Vacuity analysis for property qualification by mutation of checkers. In: Design, automation test in Europe conference exhibition (DATE), pp\u00a0478\u2013483","DOI":"10.1109\/DATE.2010.5457158"},{"key":"23_CR43","doi-asserted-by":"crossref","unstructured":"Di\u00a0Guglielmo L, Fummi F, Pravadelli G, Stefanni F, Vinco S (2012) A formal support for homogeneous simulation of heterogeneous embedded systems. In: IEEE international symposium on industrial embedded systems (SIES), pp\u00a0211\u2013219","DOI":"10.1109\/SIES.2012.6356587"},{"issue":"2","key":"23_CR44","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1109\/TC.2012.156","volume":"62","author":"L Di Guglielmo","year":"2013","unstructured":"Di\u00a0Guglielmo L, Fummi F, Pravadelli G, Stefanni F, Vinco S (2013) UNIVERCM: the universal versatile computational model for heterogeneous system integration. IEEE Trans Comput 62(2):225\u2013241","journal-title":"IEEE Trans Comput"},{"issue":"3","key":"23_CR45","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1007\/s10617-014-9158-1","volume":"19","author":"E Ebeid","year":"2015","unstructured":"Ebeid E, Fummi F, Quaglia D (2015) HDL code generation from UML\/MARTE sequence diagrams for verification and synthesis. Des Autom Embed Syst 19(3):277\u2013299. DOI 10.1007\/s10617-014-9158-1","journal-title":"Des Autom Embed Syst"},{"issue":"4","key":"23_CR46","doi-asserted-by":"publisher","first-page":"603","DOI":"10.1109\/TCAD.2015.2394395","volume":"34","author":"E Ebeid","year":"2015","unstructured":"Ebeid E, Fummi F, Quaglia D (2015) Model-driven design of network aspects of distributed embedded systems. IEEE Trans Comput Aided Des Integr Circuits Syst 34(4):603\u2013614","journal-title":"IEEE Trans Comput Aided Des Integr Circuits Syst"},{"issue":"4","key":"23_CR47","doi-asserted-by":"publisher","first-page":"42","DOI":"10.1109\/MC.2009.118","volume":"42","author":"C Ebert","year":"2009","unstructured":"Ebert C, Jones C (2009) Embedded software: facts, figures, and future. Computer 42(4):42\u201352","journal-title":"Computer"},{"issue":"4","key":"23_CR48","doi-asserted-by":"publisher","first-page":"528","DOI":"10.1109\/TC.2007.1012","volume":"56","author":"A Fedeli","year":"2007","unstructured":"Fedeli A, Fummi F, Pravadelli G (2007) Properties incompleteness evaluation by functional verification. IEEE Trans Comput 56(4):528\u2013544","journal-title":"IEEE Trans Comput"},{"key":"23_CR49","volume-title":"From conception to implementation: a model based design approach","author":"A Ferrari","year":"2004","unstructured":"Ferrari A, Gaviani G, Gentile G, Stara G, Romagnoli G, Thomsen T (2004) From conception to implementation: a model based design approach. In: Proceedings of IFAC symposium on advances in automotive control"},{"key":"23_CR50","first-page":"213","volume":"63","author":"L Ferro","year":"2010","unstructured":"Ferro L, Pierre L (2010) ISIS: runtime verification of TLM platforms. Adv Des Methods Model Lang Embed Syst SoCs 63:213\u2013226","journal-title":"Adv Des Methods Model Lang Embed Syst SoCs"},{"key":"23_CR51","volume-title":"Assertion-based design","author":"H Foster","year":"2004","unstructured":"Foster H, Krolnik A, Lacey D (2004) Assertion-based design. Springer, New York"},{"key":"23_CR52","unstructured":"Foster H, Larsen K, Turpin M (2006) Introducing the new accellera open verification library standard. In: Proceedings of design and verification conference (DVCON)"},{"key":"23_CR53","unstructured":"Gentleware (2012) Poseidon for UML embedded edition. http:\/\/www.gentleware.com\/uml-software-embedded-edition.html"},{"key":"23_CR54","doi-asserted-by":"crossref","unstructured":"Godefroid P, Klarlund N, Sen K (2005) DART: directed automated random testing. In: Proceedings of ACM SIGPLAN conference on programming language, design, and implementation (PLDI), pp\u00a0213\u2013223","DOI":"10.1145\/1065010.1065036"},{"issue":"6","key":"23_CR55","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1109\/MS.2003.1241368","volume":"20","author":"B Graaf","year":"2003","unstructured":"Graaf B, Lormans M, Toetenel H (2003) Embedded software engineering: the state of the practice. IEEE Softw 20(6):61\u201369","journal-title":"IEEE Softw"},{"key":"23_CR56","first-page":"33","volume-title":"UNIVERCM: The UNIversal VERsatile computational model for heterogeneous embedded system design","author":"L Di Guglielmo","year":"2011","unstructured":"Di Guglielmo L, Fummi F, Pravadelli G, Stefanni F, Vinco S (2011) UNIVERCM: The UNIversal VERsatile computational model for heterogeneous embedded system design. In: Proceedings of IEEE HLDVT, pp\u00a033\u201340"},{"key":"23_CR57","unstructured":"HAL \u2013 Inria (2012) Gaspard2 UML profile documentation. http:\/\/hal.inria.fr\/inria-00171137\/en"},{"key":"23_CR58","first-page":"278","volume-title":"Logic in computer science (LICS)","author":"T Henzinger","year":"1996","unstructured":"Henzinger T (1996) The theory of hybrid automata. In: Logic in computer science (LICS). IEEE Computer Society, New Brunswick, pp\u00a0278\u2013292"},{"key":"23_CR59","doi-asserted-by":"crossref","unstructured":"Hiller M (2000) Executable assertions for detecting data errors in embedded control systems. In: Proceedings of IEEE international conference on dependable systems and networks (DSN), pp\u00a024\u201333","DOI":"10.1109\/ICDSN.2000.857510"},{"key":"23_CR60","first-page":"300","volume-title":"Coverage estimation for symbolic model checking","author":"Y Hoskote","year":"1999","unstructured":"Hoskote Y, Kam T, Ho P, Zhao X (1999) Coverage estimation for symbolic model checking. In: Proceedings ACM\/IEEE design automation conference, pp\u00a0300\u2013305"},{"issue":"9","key":"23_CR61","doi-asserted-by":"publisher","first-page":"733","DOI":"10.1109\/TSE.2006.92","volume":"32","author":"D Hyunsook","year":"2006","unstructured":"Hyunsook D, Rothermel G (2006) On the use of mutation faults in empirical assessments of test case prioritization techniques. IEEE Trans Softw Eng 32(9):733\u2013752","journal-title":"IEEE Trans Softw Eng"},{"key":"23_CR62","unstructured":"IAR Systems (2012) IAR visualSTATE. http:\/\/www.iar.com\/Products\/IAR-visualSTATE\/"},{"key":"23_CR63","unstructured":"IBM (2012) Rational Rhapsody. http:\/\/www.ibm.com\/software\/awdtools\/rhapsody"},{"key":"23_CR64","unstructured":"IEEE Computer Society (2010) IEEE Standard for Property Specification Language (PSL) (IEEE Std 1850-2010)"},{"key":"23_CR65","doi-asserted-by":"crossref","unstructured":"Jayakumar N, Purandare M, Somenzi F (2003) Dos and don\u2019ts of CTL state coverage estimation. In: Proceedings of design automation conference (DAC)","DOI":"10.1145\/775905.775908"},{"key":"23_CR66","first-page":"280","volume-title":"Have I written enough properties? \u2013 a method of comparison between specification and implementation","author":"S Katz","year":"1999","unstructured":"Katz S, Grumberg O (1999) Have I written enough properties? \u2013 a method of comparison between specification and implementation. In: Proceedings ACM advanced research working conference on correct hardware design and verification methods. Springer, pp\u00a0280\u2013297"},{"issue":"2","key":"23_CR67","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1109\/TSE.2010.68","volume":"37","author":"M Kim","year":"2011","unstructured":"Kim M, Kim Y, Kim H (2011) A comparative study of software model checkers as unit testing tools: an industrial case study. IEEE Trans Softw Eng 37(2):146\u2013160","journal-title":"IEEE Trans Softw Eng"},{"issue":"7","key":"23_CR68","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1145\/360248.360252","volume":"19","author":"JC King","year":"1976","unstructured":"King JC (1976) Symbolic execution and program testing. Commun ACM 19(7):385\u2013394","journal-title":"Commun ACM"},{"key":"23_CR69","first-page":"82","volume-title":"Vacuity detection in temporal model checking","author":"O Kupferman","year":"1999","unstructured":"Kupferman O, Vardi MY (1999) Vacuity detection in temporal model checking. In: Conference on correct hardware design and verification methods, pp\u00a082\u201396"},{"issue":"2","key":"23_CR70","doi-asserted-by":"publisher","first-page":"224","DOI":"10.1007\/s100090100062","volume":"4","author":"O Kupferman","year":"2003","unstructured":"Kupferman O, Vardi M (2003) Vacuity detection in temporal model checking. Int J Softw Tools Technol Transfer 4(2):224\u2013233","journal-title":"Int J Softw Tools Technol Transfer"},{"key":"23_CR71","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2008.ECP.29","volume-title":"A theory of mutations with applications to vacuity, coverage, and fault tolerance","author":"O Kupferman","year":"2008","unstructured":"Kupferman O, Li W, Seshia S (2008) A theory of mutations with applications to vacuity, coverage, and fault tolerance. In: Proceedings IEEE international conference on formal methods in computer-aided design"},{"key":"23_CR72","doi-asserted-by":"crossref","unstructured":"Lattner C, Adve V (2005) The LLVM compiler framework and infrastructure tutorial. In: Proceedings of international workshop on languages and compilers for high performance computing (LCPC). Springer, pp\u00a015\u201316","DOI":"10.1007\/11532378_2"},{"key":"23_CR73","first-page":"354","volume-title":"Mutation coverage estimation for model checking","author":"T Lee","year":"2004","unstructured":"Lee T, Hsiung P (2004) Mutation coverage estimation for model checking. In: Proceedings international symposium on automated technology for verification and analysis, pp\u00a0354\u2013368"},{"key":"23_CR74","doi-asserted-by":"crossref","unstructured":"Lettnin D, Nalla P, Ruf J, Kropf T, Rosenstiel W, Kirsten T, Schonknecht V, Reitemeyer S (2008) Verification of temporal properties in automotive embedded software. In: Proceedings of design, automation & test in Europe conference & exhibition (DATE). ACM, pp\u00a0164\u2013169","DOI":"10.1145\/1403375.1403417"},{"key":"23_CR75","first-page":"119","volume-title":"An empirical study on testing and fault tolerance for software reliability engineering","author":"MR Lyu","year":"2003","unstructured":"Lyu MR, Zubin H, Sze SKS, Xia C (2003) An empirical study on testing and fault tolerance for software reliability engineering. In: Proceedings of IEEE ISSRE, pp\u00a0119\u2013130"},{"issue":"2","key":"23_CR76","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1002\/stvr.308","volume":"15","author":"YS Ma","year":"2005","unstructured":"Ma YS, Offutt J, Kwon YR (2005) Mujava: an automated class mutation system. Softw Test Verif Reliab 15(2):97\u2013133","journal-title":"Softw Test Verif Reliab"},{"key":"23_CR77","doi-asserted-by":"crossref","unstructured":"Majumdar R, Sen K (2007) Hybrid concolic testing. In: Proceedings of IEEE international conference on software engineering (ICSE), pp\u00a0416\u2013426","DOI":"10.1109\/ICSE.2007.41"},{"key":"23_CR78","doi-asserted-by":"crossref","unstructured":"Mathur AP (1991) Performance, effectiveness, and reliability issues in software testing. In: COMPSAC\u201991, pp\u00a0604\u2013605","DOI":"10.1109\/CMPSAC.1991.170248"},{"issue":"2","key":"23_CR79","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1002\/stvr.294","volume":"14","author":"P McMinn","year":"2004","unstructured":"McMinn P (2004) Search-based software test data generation: a survey. Softw Test Verif Reliab 14(2):105\u2013156","journal-title":"Softw Test Verif Reliab"},{"key":"23_CR80","unstructured":"Mentor Graphics (2012) Assertion-based verification. http:\/\/www.mentor.com\/products\/fv\/methodologies\/abv"},{"key":"23_CR81","unstructured":"Mischkalla F, He D, Mueller W (2010) A UML profile for SysML-based comodeling for embedded systems simulation and synthesis. In: Proceedings of workshop on model based engineering for embedded system design (MBED)"},{"key":"23_CR82","first-page":"99","volume-title":"Automatic functional test program generation for pipelined processors using model checking","author":"P Mishra","year":"2002","unstructured":"Mishra P, Dutt N (2002) Automatic functional test program generation for pipelined processors using model checking. In: Proceedings IEEE high-level design validation and test, pp\u00a099\u2013103"},{"key":"23_CR83","unstructured":"Object Management Group, Inc. (2012) MARTE resource page. http:\/\/www.omgmarte.org\/"},{"key":"23_CR84","unstructured":"Object Management Group, Inc. (2012) OMG specifications. http:\/\/www.omg.org"},{"key":"23_CR85","unstructured":"Object Management Group, Inc. (2012) UML resource page. http:\/\/www.uml.org"},{"key":"23_CR86","doi-asserted-by":"publisher","first-page":"34","DOI":"10.1007\/978-1-4757-5939-6_7","volume-title":"Mutation testing for the new century","author":"AJ Offutt","year":"2001","unstructured":"Offutt AJ, Untch RH (2001) Mutation 2000: uniting the orthogonal. In: Wong WE (ed) Mutation testing for the new century. Kluwer Academic Publishers, Boston, pp\u00a034\u201344"},{"key":"23_CR87","doi-asserted-by":"crossref","unstructured":"Offutt AJ, Rothermel G, Zapf C (1993) An experimental evaluation of selective mutation. In: ICSE\u201993, pp\u00a0100\u2013107","DOI":"10.1109\/ICSE.1993.346062"},{"key":"23_CR88","first-page":"222","volume-title":"System level mutation analysis applied to a state-based language","author":"T Olsson","year":"2001","unstructured":"Olsson T, Runeson P (2001) System level mutation analysis applied to a state-based language. In: Proceedings of IEEE ECBS, pp\u00a0222\u2013228"},{"key":"23_CR89","doi-asserted-by":"crossref","unstructured":"Pinto Ferraz Fabbri SC, Delamaro ME, Maldonado JC, Masiero PC (1994) Mutation analysis testing for finite state machines. In: IEEE ISSRE\u201994, pp\u00a0220\u2013229","DOI":"10.1109\/ISSRE.1994.341378"},{"issue":"4","key":"23_CR90","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1550987.1550993","volume":"8","author":"E Riccobene","year":"2009","unstructured":"Riccobene E, Scandurra P, Bocchio S, Rosti A, Lavazza L, Mantellini L (2009) SystemC\/C-based model-driven design for embedded systems. ACM Trans Embed Comput Syst 8(4):1\u201337","journal-title":"ACM Trans Embed Comput Syst"},{"key":"23_CR91","first-page":"161","volume-title":"Integrating design and verification \u2013 from simple idea to practical system","author":"C Seger","year":"2006","unstructured":"Seger C (2006) Integrating design and verification \u2013 from simple idea to practical system. In: Proceedings of ACM\/IEEE MEMOCODE, pp\u00a0161\u2013162"},{"issue":"5","key":"23_CR92","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1109\/MS.2003.1231146","volume":"20","author":"B Selic","year":"2003","unstructured":"Selic B (2003) The pragmatics of model-driven development. IEEE Softw 20(5):19\u201325","journal-title":"IEEE Softw"},{"key":"23_CR93","doi-asserted-by":"publisher","first-page":"419","DOI":"10.1007\/11817963_38","volume-title":"Proceedings of international conference on computer aided verification (CAV)","author":"K Sen","year":"2006","unstructured":"Sen K, Agha G (2006) CUTE and jCUTE: Concolic unit testing and explicit path model-checking tools. In: Proceedings of international conference on computer aided verification (CAV). Springer, Berlin\/New York, pp\u00a0419\u2013423"},{"key":"23_CR94","unstructured":"Society IC (2009) IEEE standard for system verilog-unified hardware design, specification, and verification language (IEEE Std 1800-2009)"},{"key":"23_CR95","unstructured":"Sparx Systems (2012) Enterprise architet. http:\/\/www.sparxsystems.com.au"},{"key":"23_CR96","unstructured":"STM Products (2012) radCHECK. http:\/\/www.verificationsuite.com"},{"key":"23_CR97","unstructured":"SysML Partners (2012) SysML resource page. http:\/\/www.sysml.org"},{"key":"23_CR98","unstructured":"The MathWorks, Inc. (2012) Simulink. http:\/\/www.mathworks.com\/products\/simulink\/"},{"key":"23_CR99","doi-asserted-by":"crossref","unstructured":"Tillmann N, De\u00a0Halleux J (2008) Pex: white box test generation for. NET. In: Proceedings of ACM international conference on tests and proofs (TAP), pp\u00a0134\u2013153","DOI":"10.1007\/978-3-540-79124-9_10"},{"key":"23_CR100","unstructured":"Winterholer M (2006) Transaction-based hardware software co-verification. In: Proceedings of forum on specification & design languages (FDL)"},{"key":"23_CR101","doi-asserted-by":"crossref","unstructured":"Xie F, Liu H (2007) Unified property specification for hardware\/software co-verification. In: Proceedings of international computer software and applications conference (COMSAC), pp\u00a0483\u2013490","DOI":"10.1109\/COMPSAC.2007.231"},{"key":"23_CR102","first-page":"259","volume-title":"Transition traversal coverage estimation for symbolic model checking","author":"X Xu","year":"2005","unstructured":"Xu X, Kimura S, Horikawa K, Tsuchiya T (2005) Transition traversal coverage estimation for symbolic model checking. In: Proceedings ACM\/IEEE international conference on formal methods and models for co-design, pp\u00a0259\u2013260"},{"key":"23_CR103","first-page":"1","volume-title":"Transition-based coverage estimation for symbolic model checking","author":"X Xu","year":"2006","unstructured":"Xu X, Kimura S, Horikawa K, Tsuchiya T (2006) Transition-based coverage estimation for symbolic model checking. In: Proceedings ACM\/IEEE Asia and South Pacific conference on design automation, pp\u00a01\u20136"}],"container-title":["Handbook of Hardware\/Software Codesign"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-94-017-7267-9_23","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,10,16]],"date-time":"2026-10-16T09:18:55Z","timestamp":1792142335000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/chapter\/10.1007\/978-94-017-7267-9_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9789401772662","9789401772679"],"references-count":103,"URL":"https:\/\/doi.org\/10.1007\/978-94-017-7267-9_23","relation":{},"subject":[],"published":{"date-parts":[[2017]]},"assertion":[{"value":"27 September 2017","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}