{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,9]],"date-time":"2026-02-09T00:56:23Z","timestamp":1770598583460,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642324680","type":"print"},{"value":"9783642324697","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-32469-7_6","type":"book-chapter","created":{"date-parts":[[2012,8,21]],"date-time":"2012-08-21T21:07:27Z","timestamp":1345583247000},"page":"78-92","source":"Crossref","is-referenced-by-count":19,"title":["Tool Chain to Support Automated Formal Verification of Avionics Simulink Designs"],"prefix":"10.1007","author":[{"given":"Jiri","family":"Barnat","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jan","family":"Beran","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lubos","family":"Brim","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tomas","family":"Kratochv\u00edla","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Petr","family":"Ro\u010dkai","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"6_CR1","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)"},{"key":"6_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 (Tool Paper). In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 278\u2013281. Springer, Heidelberg (2006)"},{"key":"6_CR3","doi-asserted-by":"crossref","unstructured":"Bhatt, D., Madl, G., Oglesby, D., Schloegel, K.: Towards Scalable Verification of Commercial Avionics Software (2010), http:\/\/www.ics.uci.edu\/~gabe\/papers\/BMOS_AIAA_2010.pdf","DOI":"10.2514\/6.2010-3452"},{"key":"6_CR4","unstructured":"Bhatt, D., Schloegel, K.: Effective Verification of Flight Critical Software Systems: Issues and Approaches. Presented at NSF\/Microsoft Research Workshop on Usable Verification (November 2010)"},{"key":"6_CR5","doi-asserted-by":"crossref","unstructured":"Bingham, B., Bingham, J., de Paula, F.M., Erickson, J., Singh, M., Reitblatt, G.: Industrial Strength Distributed Explicit State Model Checking. In: Parallel and Distributed Methods in Verification and High Performance Computational Systems Biology (HiBi\/PDMC), pp. 28\u201336. IEEE (2010)","DOI":"10.1109\/PDMC-HiBi.2010.13"},{"key":"6_CR6","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1007\/s10703-006-0027-9","volume":"30","author":"Y. Choi","year":"2007","unstructured":"Choi, Y.: From NuSMV to SPIN: Experiences with model checking flight guidance systems. Formal Methods in System Design\u00a030, 199\u2013216 (2007)","journal-title":"Formal Methods in System Design"},{"key":"6_CR7","doi-asserted-by":"crossref","unstructured":"Ciardo, G., Zhao, Y., Jin, X.: Parallel symbolic state-space exploration is difficult, but what is the alternative? In: Parallel and Distributed Methods in Verification (PDMC). EPTCS, vol.\u00a014, pp. 1\u201317 (2009)","DOI":"10.4204\/EPTCS.14.1"},{"key":"6_CR8","unstructured":"Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT press (1999)"},{"key":"6_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"76","DOI":"10.1007\/978-3-642-16164-3_6","volume-title":"Model Checking Software","author":"D. Cofer","year":"2010","unstructured":"Cofer, D.: Model Checking: Cleared for Take Off. In: van de Pol, J., Weber, M. (eds.) SPIN 2010. LNCS, vol.\u00a06349, pp. 76\u201387. Springer, Heidelberg (2010)"},{"key":"6_CR10","unstructured":"Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: A System of Specification Patterns (1998), http:\/\/www.cis.ksu.edu\/santos\/spec-patterns"},{"key":"6_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"122","DOI":"10.1007\/11563228_10","volume-title":"Computer Safety, Reliability, and Security","author":"A. Joshi","year":"2005","unstructured":"Joshi, A., Heimdahl, M.P.E.: Model-Based Safety Analysis of Simulink Models Using SCADE Design Verifier. In: Winther, R., Gran, B.A., Dahll, G. (eds.) SAFECOMP 2005. LNCS, vol.\u00a03688, pp. 122\u2013135. Springer, Heidelberg (2005)"},{"key":"6_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"144","DOI":"10.1007\/978-3-540-85114-1_12","volume-title":"Model Checking Software","author":"M. Kim","year":"2008","unstructured":"Kim, M., Choi, Y., Kim, Y., Kim, H.: Formal Verification of a Flash Memory Device Driver \u2013 An Experience Report. In: Havelund, K., Majumdar, R. (eds.) SPIN 2008. LNCS, vol.\u00a05156, pp. 144\u2013159. Springer, Heidelberg (2008)"},{"key":"6_CR13","doi-asserted-by":"crossref","unstructured":"Konrad, S., Cheng, B.H.C.: Real-time specification patterns. In: Proceedings of the 27th International Conference on Software Engineering, ICSE 2005, pp. 372\u2013381. ACM, New York (2005)","DOI":"10.1145\/1062455.1062526"},{"key":"6_CR14","unstructured":"Mathworks. Simulink, http:\/\/www.mathworks.com\/products\/simulink\/"},{"key":"6_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"443","DOI":"10.1007\/978-3-642-00768-2_36","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S.P. Miller","year":"2009","unstructured":"Miller, S.P.: Bridging the Gap Between Model-Based Development and Model Checking. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol.\u00a05505, pp. 443\u2013453. Springer, Heidelberg (2009)"},{"key":"6_CR16","doi-asserted-by":"crossref","unstructured":"Pingree, P., Mikk, E., Holzmann, G., Smith, M., Dams, D.: Validation of mission critical software design and implementation using model checking. In: Proc. Digital Avionics Systems Conference, pp. 6A4-1\u20136A4-12. IEEE Computer Society (2002)","DOI":"10.1109\/DASC.2002.1067982"},{"key":"6_CR17","unstructured":"SCADE. Design verifier, http:\/\/www.esterel-technologies.com\/products\/scade-suite\/add-on-modules\/design-verifier"},{"key":"6_CR18","doi-asserted-by":"crossref","unstructured":"Scaife, N., Sofronis, C., Caspi, P., Tripakis, S., Maraninchi, F.: Defining and translating a \u201dsafe\u201d subset of simulink\/stateflow into lustre. In: EMSOFT, pp. 259\u2013268. ACM (2004)","DOI":"10.1145\/1017753.1017795"},{"key":"6_CR19","doi-asserted-by":"crossref","unstructured":"Schlenoff, C., Gruninger, M., Tissot, F., Valois, J., Road, T.C., Inc, S., Lubell, J., Lee, J.: The Process Specification Language (PSL) Overview and Version 1.0 Specification (1999)","DOI":"10.6028\/NIST.IR.6459"},{"key":"6_CR20","doi-asserted-by":"crossref","unstructured":"Sims, S., Cleaveland, R., Butts, K., Ranville, S.: Automated validation of software models. In: ASE, pp. 91\u2013102. IEEE Computer Society (2001)","DOI":"10.1109\/ASE.2001.989794"},{"key":"6_CR21","doi-asserted-by":"crossref","unstructured":"Verstoep, K., Bal, H., Barnat, J., Brim, L.: Efficient Large-Scale Model Checking. In: 23rd IEEE International Parallel & Distributed Processing Symposium (IPDPS 2009). IEEE (2009)","DOI":"10.1109\/IPDPS.2009.5161000"},{"key":"6_CR22","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)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods for Industrial Critical Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-32469-7_6.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,7]],"date-time":"2025-04-07T01:35:54Z","timestamp":1743989754000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-32469-7_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642324680","9783642324697"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-32469-7_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012]]}}}