{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T19:58:07Z","timestamp":1762459087133},"publisher-location":"Berlin, Heidelberg","reference-count":31,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642397981"},{"type":"electronic","value":"9783642397998"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-39799-8_21","type":"book-chapter","created":{"date-parts":[[2013,7,10]],"date-time":"2013-07-10T19:13:06Z","timestamp":1373483586000},"page":"296-312","source":"Crossref","is-referenced-by-count":16,"title":["System Level Formal Verification via Model Checking Driven Simulation"],"prefix":"10.1007","author":[{"given":"Toni","family":"Mancini","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Federico","family":"Mari","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Annalisa","family":"Massini","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Igor","family":"Melatti","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Fabio","family":"Merli","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Enrico","family":"Tronci","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"doi-asserted-by":"crossref","unstructured":"Alur, R.: Formal verification of hybrid systems. In: Proc. EMSOFT 2011. ACM (2011)","key":"21_CR1","DOI":"10.1145\/2038642.2038685"},{"key":"21_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"278","DOI":"10.1007\/11817963_26","volume-title":"Computer Aided Verification","author":"J. Barnat","year":"2006","unstructured":"Barnat, J., Brim, L., \u010cern\u00e1, I., Moravec, P., Ro\u010dkai, P., \u0160ime\u010dek, P.: diVinE \u2013 A tool for distributed verification. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 278\u2013281. Springer, Heidelberg (2006)"},{"doi-asserted-by":"crossref","unstructured":"Bingham, B., Bingham, J., De Paula, F.M., Erickson, J., Singh, G., Reitblatt, M.: Industrial strength distributed explicit state model checking. In: Proc. PDMC-HIBI\u00a02010. IEEE (2010)","key":"21_CR3","DOI":"10.1109\/PDMC-HiBi.2010.13"},{"key":"21_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"208","DOI":"10.1007\/978-3-642-17071-3_11","volume-title":"Formal Methods for Components and Objects","author":"A. Brillout","year":"2010","unstructured":"Brillout, A., He, N., Mazzucchi, M., Kroening, D., Purandare, M., R\u00fcmmer, P., Weissenbacher, G.: Mutation-based test case generation for simulink models. In: de Boer, F.S., Bonsangue, M.M., Hallerstede, S., Leuschel, M. (eds.) FMCO 2009. LNCS, vol.\u00a06286, pp. 208\u2013227. Springer, Heidelberg (2010)"},{"key":"21_CR5","series-title":"Lecture Notes in Computer Science","volume-title":"Model-Based Testing of Reactive Systems","year":"2005","unstructured":"Broy, M., Jonsson, B., Katoen, J.-P., Leucker, M., Pretschner, A. (eds.): Model-Based Testing of Reactive Systems. LNCS, vol.\u00a03472. Springer, Heidelberg (2005)"},{"unstructured":"Cavaliere, F., Mari, F., Melatti, I., Minei, G., Salvo, I., Tronci, E., Verzino, G., Yushtein, Y.: Model checking satellite operational procedures. In: Proc. DASIA 2011 (2011)","key":"21_CR6"},{"doi-asserted-by":"crossref","unstructured":"De Paula, F.M., Hu, A.J.: An effective guidance strategy for abstraction-guided simulation. In: Proc. DAC\u00a02007, pp. 63\u201368. ACM (2007)","key":"21_CR7","DOI":"10.1109\/DAC.2007.375126"},{"unstructured":"Dean, J., Ghemawat, S.: Mapreduce: simplified data processing on large clusters. In: Proc. OSDI\u00a02004. USENIX Association (2004)","key":"21_CR8"},{"issue":"4","key":"21_CR9","doi-asserted-by":"publisher","first-page":"320","DOI":"10.1007\/s10009-004-0149-6","volume":"6","author":"G. Penna Della","year":"2004","unstructured":"Della Penna, G., Intrigila, B., Melatti, I., Tronci, E., Zilli, M.: Exploiting transition locality in automatic verification of finite state concurrent systems. STTT\u00a06(4), 320\u2013341 (2004)","journal-title":"STTT"},{"unstructured":"Dill, D.L., Drexler, A.J., Hu, A.J., Han Yang, C.: Protocol verification as a hardware design aid. In: Proc. IEEE Int. Conf. Comp. Design on VLSI in Comp. & Proc., 1991. IEEE (1992)","key":"21_CR10"},{"key":"21_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"204","DOI":"10.1007\/978-3-540-70545-1_19","volume-title":"Computer Aided Verification","author":"A.A. Gadkari","year":"2008","unstructured":"Gadkari, A.A., Yeolekar, A., Suresh, J., Ramesh, S., Mohalik, S., Shashidhar, K.C.: AutoMOTGen: Automatic model oriented test generator for embedded control systems. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol.\u00a05123, pp. 204\u2013208. Springer, Heidelberg (2008)"},{"key":"21_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1007\/978-3-540-31980-1_18","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R. Grosu","year":"2005","unstructured":"Grosu, R., Smolka, S.A.: Monte carlo model checking. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol.\u00a03440, pp. 271\u2013286. Springer, Heidelberg (2005)"},{"unstructured":"Ho, P.H., Shiple, T., Harer, K., Kukula, J., Damiano, R., Bertacco, V., Taylor, J., Long, J.: Smart simulation using collaborative formal and simulation engines. In: Proc. ICCAD 2000 (2000)","key":"21_CR13"},{"unstructured":"Holzmann, G.J.: The SPIN model checker. Addison-Wesley (2003)","key":"21_CR14"},{"key":"21_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1007\/978-3-642-31759-0_12","volume-title":"Model Checking Software","author":"G.J. Holzmann","year":"2012","unstructured":"Holzmann, G.J.: Parallelizing the spin model checker. In: Donaldson, A., Parker, D. (eds.) SPIN 2012. LNCS, vol.\u00a07385, pp. 155\u2013171. Springer, Heidelberg (2012)"},{"issue":"3-4","key":"21_CR16","doi-asserted-by":"publisher","first-page":"283","DOI":"10.1007\/s10515-008-0033-9","volume":"15","author":"G.J. Holzmann","year":"2008","unstructured":"Holzmann, G.J., Joshi, R., Groce, A.: Model driven code checking. Autom. Softw. Eng.\u00a015(3-4), 283\u2013297 (2008)","journal-title":"Autom. Softw. Eng."},{"key":"21_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"430","DOI":"10.1007\/978-3-642-02658-4_33","volume-title":"Computer Aided Verification","author":"A. Kanade","year":"2009","unstructured":"Kanade, A., Alur, R., Ivan\u010di\u0107, F., Ramesh, S., Sankaranarayanan, S., Shashidhar, K.C.: Generating and analyzing symbolic traces of simulink\/Stateflow models. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol.\u00a05643, pp. 430\u2013445. Springer, Heidelberg (2009)"},{"key":"21_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"152","DOI":"10.1007\/978-3-540-30206-3_12","volume-title":"Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems","author":"O. Maler","year":"2004","unstructured":"Maler, O., Nickovic, D.: Monitoring temporal properties of continuous signals. In: Lakhnech, Y., Yovine, S. (eds.) FORMATS 2004 and FTRTFT 2004. LNCS, vol.\u00a03253, pp. 152\u2013166. Springer, Heidelberg (2004)"},{"key":"21_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"606","DOI":"10.1007\/11901433_33","volume-title":"Formal Methods and Software Engineering","author":"B. Meenakshi","year":"2006","unstructured":"Meenakshi, B., Bhatnagar, A., Roy, S.: Tool for translating simulink models into input language of a model checker. In: Liu, Z., Kleinberg, R.D. (eds.) ICFEM 2006. LNCS, vol.\u00a04260, pp. 606\u2013620. Springer, Heidelberg (2006)"},{"issue":"1","key":"21_CR20","doi-asserted-by":"publisher","first-page":"13","DOI":"10.1007\/s10009-008-0094-x","volume":"11","author":"I. Melatti","year":"2009","unstructured":"Melatti, I., Palmer, R., Sawaya, G., Yang, Y., Kirby, R.M., Gopalakrishnan, G.: Parallel and distributed model checking in eddy. Int. J. Softw. Tools Technol. Transf.\u00a011(1), 13\u201325 (2009)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"doi-asserted-by":"crossref","unstructured":"Nanshi, K., Somenzi, F.: Guiding simulation with increasingly refined abstract traces. In: Proc. DAC\u00a02006, pp. 737\u2013742. ACM (2006)","key":"21_CR21","DOI":"10.1109\/DAC.2006.229318"},{"doi-asserted-by":"crossref","unstructured":"Rozier, K.Y., Vardi, M.Y.: Deterministic compilation of temporal safety properties in explicit state model checking. In: Proc. HVC\u00a02012. Springer (2012)","key":"21_CR22","DOI":"10.1007\/978-3-642-39611-3_23"},{"key":"21_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"266","DOI":"10.1007\/11513988_26","volume-title":"Computer Aided Verification","author":"K. Sen","year":"2005","unstructured":"Sen, K., Viswanathan, M., Agha, G.: On statistical model checking of stochastic systems. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 266\u2013280. Springer, Heidelberg (2005)"},{"doi-asserted-by":"crossref","unstructured":"Sontag, E.D.: Mathematical Control Theory: Deterministic Finite Dimensional Systems. Texts in Applied Mathematics. Springer (1998)","key":"21_CR24","DOI":"10.1007\/978-1-4612-0577-7"},{"issue":"2","key":"21_CR25","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1023\/A:1008771324652","volume":"18","author":"U. Stern","year":"2001","unstructured":"Stern, U., Dill, D.L.: Parallelizing the Murphi Verifier. Form. Methods Syst. Des.\u00a018(2), 117\u2013129 (2001)","journal-title":"Form. Methods Syst. Des."},{"issue":"4","key":"21_CR26","doi-asserted-by":"publisher","first-page":"779","DOI":"10.1145\/1113830.1113834","volume":"4","author":"S. Tripakis","year":"2005","unstructured":"Tripakis, S., Sofronis, C., Caspi, P., Curic, A.: Translating discrete-time Simulink to Lustre. ACM Trans. Emb. Comp. Syst.\u00a04(4), 779\u2013818 (2005)","journal-title":"ACM Trans. Emb. Comp. Syst."},{"unstructured":"Tronci, E., Della Penna, G., Intrigila, B., Zilli, M.: A probabilistic approach to automatic verification of concurrent systems. In: Proc. APSEC\u00a02001, pp. 317\u2013324. IEEE (2001)","key":"21_CR27"},{"doi-asserted-by":"crossref","unstructured":"Venkatesh, R., Shrotri, U., Darke, P., Bokil, P.: Test generation for large automotive models. In: Proc. ICIT\u00a02012, pp. 662\u2013667. IEEE (2012)","key":"21_CR28","DOI":"10.1109\/ICIT.2012.6210014"},{"key":"21_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1007\/978-3-540-79707-4_7","volume-title":"Formal Methods for Industrial Critical Systems","author":"M. Whalen","year":"2008","unstructured":"Whalen, M., Cofer, D., Miller, S., Krogh, B.H., Storm, W.: Integration of formal analysis into a model-based software development process. In: Leue, S., Merino, P. (eds.) FMICS 2007. LNCS, vol.\u00a04916, pp. 68\u201384. Springer, Heidelberg (2008)"},{"doi-asserted-by":"crossref","unstructured":"Yang, C.H., Dill, D.L.: Validation with guided search of the state space. In: Proc. DAC\u00a01998, pp. 599\u2013604. ACM (1998)","key":"21_CR30","DOI":"10.1145\/277044.277201"},{"doi-asserted-by":"crossref","unstructured":"Zuliani, P., Platzer, A., Clarke, E.M.: Bayesian statistical model checking with application to simulink\/stateflow verification. In: Proc. HSCC\u00a02010, pp. 243\u2013252 (2010)","key":"21_CR31","DOI":"10.21236\/ADA531406"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-39799-8_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,15]],"date-time":"2019-05-15T14:20:54Z","timestamp":1557930054000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-39799-8_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642397981","9783642397998"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-39799-8_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}