{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,20]],"date-time":"2026-01-20T11:12:43Z","timestamp":1768907563471,"version":"3.49.0"},"publisher-location":"Cham","reference-count":33,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319175232","type":"print"},{"value":"9783319175249","type":"electronic"}],"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-319-17524-9_13","type":"book-chapter","created":{"date-parts":[[2015,4,7]],"date-time":"2015-04-07T06:15:31Z","timestamp":1428387331000},"page":"173-187","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":28,"title":["Towards Realizability Checking of Contracts Using Theories"],"prefix":"10.1007","author":[{"given":"Andrew","family":"Gacek","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andreas","family":"Katis","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael W.","family":"Whalen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"John","family":"Backes","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Darren","family":"Cofer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,4,8]]},"reference":[{"key":"13_CR1","unstructured":"SAE-AS5506: Architecture Analysis and Design Language. SAE (2004)"},{"key":"13_CR2","volume-title":"A Practical Guide to SysML: Systems Modeling Language","author":"S Friedenthal","year":"2008","unstructured":"Friedenthal, S., Moore, A., Steiner, R.: A Practical Guide to SysML: Systems Modeling Language. Morgan Kaufmann Publishers Inc., San Francisco (2008)"},{"key":"13_CR3","unstructured":"Consortium, A.: Automotive Open System Architecture (AUTOSAR) Revision 4.2.1. AUTOSAR (2014)"},{"key":"13_CR4","doi-asserted-by":"crossref","unstructured":"Varona-Gomez, R., Villar, E.: Aadl simulation and performance analysis in systemc. In: 2009 14th IEEE International Conference on Engineering of Complex Computer Systems, pp. 323\u2013328 (2009)","DOI":"10.1109\/ICECCS.2009.11"},{"key":"13_CR5","doi-asserted-by":"publisher","first-page":"754","DOI":"10.1093\/comjnl\/bxq024","volume":"54","author":"M Bozzano","year":"2011","unstructured":"Bozzano, M., Cimatti, A., Katoen, J.P., Nguyen, V.Y., Noll, T., Roveri, M.: Safety, dependability and performance analysis of extended aadl models. Comput. J. 54, 754\u2013775 (2011)","journal-title":"Comput. J."},{"key":"13_CR6","unstructured":"Apvrille, L., Roudier, Y.: SysML-Sec: A model-driven environment for developing secure embedded systems. In: SAR-SSI 2013, 8\u00e8me Conf\u00e9rence sur la S\u00e9curit\u00e9 des Architectures R\u00e9seaux et des Syst\u00e8mes d\u2019Information, Mont-de-Marsan, France, 16\u201318 Septembre 2013"},{"key":"13_CR7","doi-asserted-by":"crossref","unstructured":"Bozzano, M., Cimatti, A., Katoen, J.P., Katsaros, P., Mokos, K., Nguyen, V.Y., Noll, T., Postma, B., Roveri, M.: Spacecraft early design validation using formal methods. Reliability Engineering and System Safety 132 (2014)","DOI":"10.1016\/j.ress.2014.07.003"},{"key":"13_CR8","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1109\/MS.2012.173","volume":"30","author":"MW Whalen","year":"2013","unstructured":"Whalen, M.W., Gacek, A., Cofer, D., Murugesan, A., Heimdahl, M.P., Rayadurgam, S.: Your what is my how: Iteration and hierarchy in system design. IEEE Software 30, 54\u201360 (2013)","journal-title":"IEEE Software"},{"key":"13_CR9","doi-asserted-by":"crossref","unstructured":"Rushby, J.: New challenges in certification for aircraft software. In: Proceedings of the Ninth ACM Int\u2019l Conf. on Embedded Software, pp. 211\u2013218. ACM (2011)","DOI":"10.1145\/2038642.2038675"},{"key":"13_CR10","doi-asserted-by":"publisher","first-page":"303","DOI":"10.1007\/s10009-004-0173-6","volume":"8","author":"SP Miller","year":"2006","unstructured":"Miller, S.P., Tribble, A.C., Whalen, M.W., Heimdahl, M.P.E.: Proving the shalls: Early validation of requirements through formal methods. Int. J. Softw. Tools Technol. Transf. 8, 303\u2013319 (2006)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"13_CR11","unstructured":"Hammond, J., Rawlings, R., Hall, A.: Will it work? [requirements engineering]. In: Proceedings of Fifth IEEE Int\u2019l Symposium on Requirements Engineering, 2001, pp. 102\u2013109 (2001)"},{"key":"13_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1007\/978-3-642-28891-3_13","volume-title":"Proceedings of the 4th NASA Formal Methods Symposium (NFM 2012)","author":"DD Cofer","year":"2012","unstructured":"Cofer, D.D., Gacek, A., Miller, S.P., Whalen, M.W., LaValley, B., Sha, L.: Compositional verification of architectural models. In: Goodloe, A.E., Person, S. (eds.) Proceedings of the 4th NASA Formal Methods Symposium (NFM 2012). LNCS, vol. 7226, pp. 126\u2013140. Springer-Verlag, Heidelberg (2012)"},{"key":"13_CR13","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Rosner, R.: On the Synthesis of a Reactive Module. In: Proceedings of the 16th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 1989), pp. 179\u2013190 (1989)","DOI":"10.1145\/75277.75293"},{"key":"13_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"652","DOI":"10.1007\/978-3-642-31424-7_45","volume-title":"Computer Aided Verification (CAV 2012)","author":"A Bohy","year":"2012","unstructured":"Bohy, A., Bruy\u00e9re, V., Filiot, E., Jin, N., Raskin, J.F.: Acacia+, a tool for LTL Synthesis. In: Madhusudan, P., Seshia, S.A. (eds.) Computer Aided Verification (CAV 2012). LNCS, vol. 7358, pp. 652\u2013657. Springer, Heidelberg (2012)"},{"key":"13_CR15","unstructured":"Hamza, J., Jobstmann, B., Kuncak, V.: Synthesis for regular specifications over unbounded domains. In: Proceedings of the 2010 Conference on Formal Methods in Computer-Aided Design, pp. 101\u2013109 (2010)"},{"key":"13_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1007\/978-3-540-71209-1_21","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2007)","author":"K Chatterjee","year":"2007","unstructured":"Chatterjee, K., Henzinger, T.A.: Assume-guarantee synthesis. In: Grumberg, O., Huth, M. (eds.) Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2007). LNCS, vol. 4424, pp. 261\u2013275. Springer, Heidelberg (2007)"},{"key":"13_CR17","doi-asserted-by":"crossref","unstructured":"Murugesan, A., Whalen, M.W., Rayadurgam, S., Heimdahl, M.P.: Compositional verification of a medical device system. In: ACM Int\u2019l Conf. on High Integrity Language Technology (HILT) 2013. ACM (2013)","DOI":"10.1145\/2527269.2527272"},{"key":"13_CR18","doi-asserted-by":"crossref","unstructured":"Katis, A., Gacek, A., Whalen, M.W.: Machine-checked proofs for realizability checking algorithms (2015) (submitted). http:\/\/arxiv.org\/abs\/1502.01292","DOI":"10.1007\/978-3-319-29613-5_7"},{"key":"13_CR19","unstructured":"Gacek, A.: JKind - a Java implementation of the KIND model checker (2014). https:\/\/github.com\/agacek\/jkind"},{"key":"13_CR20","unstructured":"Hagen, G.: Verifying safety properties of Lustre programs: an SMT-based approach. PhD thesis, University of Iowa (2008)"},{"key":"13_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L De Moura","year":"2008","unstructured":"De Moura, L., Bj\u00f8rner, N.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) Tools and Algorithms for the Construction and Analysis of Systems. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"13_CR22","doi-asserted-by":"crossref","unstructured":"Murugesan, A., Sokolsky, O., Rayadurgam, S., Whalen, M., Heimdahl, M., Lee, I.: Linking abstract analysis to concrete design: A hierarchical approach to verify medical CPS safety. In: Proceedings of ICCPS 2014 (2014)","DOI":"10.1109\/ICCPS.2014.6843718"},{"key":"13_CR23","first-page":"37","volume":"17","author":"CA Gunter","year":"2000","unstructured":"Gunter, C.A., Gunter, E.L., Jackson, M., Zave, P.: A Reference model for Requirements and Specifications. IEEE Software 17, 37\u201343 (2000)","journal-title":"IEEE Software"},{"key":"13_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1007\/978-3-642-19583-9_16","volume-title":"Hardware and Software: Verification and Testing (HVC 2010)","author":"U Klein","year":"2010","unstructured":"Klein, U., Pnueli, A.: Revisiting synthesis of GR(1) specifications. In: Barner, S., Harris, I., Kroening, D., Raz, O. (eds.) Hardware and Software: Verification and Testing (HVC 2010). LNCS, vol. 6504, pp. 161\u2013181. Springer, Heidelberg (2010)"},{"key":"13_CR25","first-page":"367","volume":"60","author":"S Tini","year":"2003","unstructured":"Tini, S., Maggiolo-Schettini, A.: Compositional Synthesis of Generalized Mealy Machines. Fundamenta Informaticae 60, 367\u2013382 (2003)","journal-title":"Fundamenta Informaticae"},{"key":"13_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"554","DOI":"10.1007\/978-3-642-27660-6_45","volume-title":"Theory and Practice of Computer Science","author":"N Bene\u0161","year":"2012","unstructured":"Bene\u0161, N., \u010cern\u00e1, I.: Factorization for component-interaction automata. In: Bielikov\u00e1, M., Friedrich, G., Gottlob, G., Katzenbeisser, S., Tur\u00e1n, G. (eds.) Theory and Practice of Computer Science. LNCS, vol. 7147, pp. 554\u2013565. Springer, Heidelberg (2012)"},{"key":"13_CR27","doi-asserted-by":"crossref","unstructured":"Aziz, A., Balarin, F., Braton, R., Sangiovanni-Vincentelli, A.: Sequential synthesis using SIS. In: Proceedings of the 1995 IEEE\/ACM International Conference on Computer-Aided Design (ICCAD 1995), pp. 612\u2013617 (1995)","DOI":"10.1109\/ICCAD.1995.480192"},{"key":"13_CR28","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Micheli, A., Roveri, M.: Solving temporal problems using SMT: Weak controllability. In: AAAI, pp. 448\u2013454 (2012)","DOI":"10.1609\/aaai.v26i1.8136"},{"key":"13_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"248","DOI":"10.1007\/978-3-642-33558-7_20","volume-title":"Principles and Practice of Constraint Programming (CP)","author":"A Cimatti","year":"2012","unstructured":"Cimatti, A., Micheli, A., Roveri, M.: Solving temporal problems using SMT: Strong controllability. In: Milano, M. (ed.) Principles and Practice of Constraint Programming (CP). LNCS, vol. 7514, pp. 248\u2013264. Springer, Heidelberg (2012)"},{"key":"13_CR30","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Micheli, A., Roveri, M.: Solving strong controllability of temporal problems with uncertainty using SMT. Constraints (2014)","DOI":"10.1007\/s10601-014-9167-5"},{"key":"13_CR31","doi-asserted-by":"crossref","unstructured":"Beyene, T., Chaudhuri, S., Popeea, C., Rybalchenko, A.: A constraint-based approach to solving games on infinite graphs. In: Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. POPL 2014, pp. 221\u2013233. ACM, New York, NY, USA (2014)","DOI":"10.1145\/2535838.2535860"},{"key":"13_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"869","DOI":"10.1007\/978-3-642-39799-8_61","volume-title":"Computer Aided Verification (CAV)","author":"TA Beyene","year":"2013","unstructured":"Beyene, T.A., Popeea, C., Rybalchenko, A.: Solving existentially quantified Horn clauses. In: Sharygina, N., Veith, H. (eds.) Computer Aided Verification (CAV). LNCS, vol. 8044, pp. 869\u2013882. Springer, Heidelberg (2013)"},{"key":"13_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1007\/978-3-642-18275-4_7","volume-title":"Verification, Model Checking, and Abstract Interpretation (VMCAI)","author":"A Bradley","year":"2011","unstructured":"Bradley, A.: SAT-based model checking without unrolling. In: Jhala, R., Schmidt, D. (eds.) Verification, Model Checking, and Abstract Interpretation (VMCAI). LNCS, vol. 6538, pp. 70\u201387. Springer, Heidelberg (2011)"}],"container-title":["Lecture Notes in Computer Science","NASA Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-17524-9_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,21]],"date-time":"2025-05-21T23:26:24Z","timestamp":1747869984000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-17524-9_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319175232","9783319175249"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-17524-9_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"8 April 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}