{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,18]],"date-time":"2026-03-18T13:22:31Z","timestamp":1773840151112,"version":"3.50.1"},"publisher-location":"Cham","reference-count":37,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319893624","type":"print"},{"value":"9783319893631","type":"electronic"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-89363-1_10","type":"book-chapter","created":{"date-parts":[[2018,4,3]],"date-time":"2018-04-03T13:04:43Z","timestamp":1522760683000},"page":"169-188","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":11,"title":["Supporting Verification-Driven Incremental Distributed Design of Components"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-5303-8481","authenticated-orcid":false,"given":"Claudio","family":"Menghi","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7922-4936","authenticated-orcid":false,"given":"Paola","family":"Spoletini","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6301-3517","authenticated-orcid":false,"given":"Marsha","family":"Chechik","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7234-5011","authenticated-orcid":false,"given":"Carlo","family":"Ghezzi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,4,4]]},"reference":[{"issue":"1","key":"10_CR1","doi-asserted-by":"crossref","first-page":"7","DOI":"10.1023\/A:1008739929481","volume":"15","author":"R Alur","year":"1999","unstructured":"Alur, R., Henzinger, T.A.: Reactive modules. Formal Meth. Softw. Des. 15(1), 7\u201348 (1999)","journal-title":"Formal Meth. Softw. Des."},{"key":"10_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"501","DOI":"10.1007\/978-3-662-46681-0_49","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R Alur","year":"2015","unstructured":"Alur, R., Moarref, S., Topcu, U.: Pattern-Based Refinement of Assume-Guarantee Specifications in Reactive Synthesis. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 501\u2013516. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_49"},{"key":"10_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1007\/978-3-319-41540-6_14","volume-title":"Computer Aided Verification","author":"R Alur","year":"2016","unstructured":"Alur, R., Moarref, S., Topcu, U.: Compositional synthesis of reactive controllers for multi-agent systems. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9780, pp. 251\u2013269. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41540-6_14"},{"issue":"6","key":"10_CR4","doi-asserted-by":"crossref","first-page":"175","DOI":"10.1145\/291252.288305","volume":"23","author":"R Alur","year":"1998","unstructured":"Alur, R., Yannakakis, M.: Model checking of hierarchical state machines. ACM SIGSOFT Softw. Eng. Notes 23(6), 175\u2013188 (1998)","journal-title":"ACM SIGSOFT Softw. Eng. Notes"},{"key":"10_CR5","doi-asserted-by":"crossref","unstructured":"Amalfitano, D., Fasolino, A.R., Tramontana, P.: Reverse engineering finite state machines from rich internet applications. In: Proceedings of the 15th Working Conference on Reverse Engineering, pp. 69\u201373 (2008)","DOI":"10.1109\/WCRE.2008.17"},{"key":"10_CR6","doi-asserted-by":"crossref","unstructured":"Bensalem, S., Bozga, M., Krichen, M., Tripakis, S.: Testing conformance of real-time applications by automatic generation of observer. In: Proceedings of RV, Electronic Notes in Theoretical Computer Science, pp. 23\u201343 (2004)","DOI":"10.1016\/j.entcs.2004.01.036"},{"key":"10_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1007\/978-3-319-66197-1_4","volume-title":"Software Engineering and Formal Methods","author":"A Bernasconi","year":"2017","unstructured":"Bernasconi, A., Menghi, C., Spoletini, P., Zuck, L.D., Ghezzi, C.: From model checking to a temporal proof for partial models. In: Cimatti, A., Sirjani, M. (eds.) SEFM 2017. LNCS, vol. 10469, pp. 54\u201369. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66197-1_4"},{"key":"10_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"274","DOI":"10.1007\/3-540-48683-6_25","volume-title":"Computer Aided Verification","author":"G Bruns","year":"1999","unstructured":"Bruns, G., Godefroid, P.: Model checking partial state spaces with 3-valued temporal logics. In: Halbwachs, N., Peled, D. (eds.) CAV 1999. LNCS, vol. 1633, pp. 274\u2013287. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48683-6_25"},{"issue":"3","key":"10_CR9","doi-asserted-by":"crossref","first-page":"235","DOI":"10.1007\/s10703-008-0053-x","volume":"32","author":"S Chaki","year":"2008","unstructured":"Chaki, S., Clarke, E.M., Sharygina, N., Sinha, N.: Verification of evolving software via component substitutability analysis. Formal Methods Softw. Des. 32(3), 235\u2013266 (2008)","journal-title":"Formal Methods Softw. Des."},{"issue":"4","key":"10_CR10","doi-asserted-by":"crossref","first-page":"371","DOI":"10.1145\/990010.990011","volume":"12","author":"M Chechik","year":"2003","unstructured":"Chechik, M., Devereux, B., Easterbrook, S., Gurfinkel, A.: Multi-valued symbolic model-checking. ACM Trans. Softw. Eng. Methodol. 12(4), 371\u2013408 (2003)","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"10_CR11","unstructured":"Ciolek, D., Braberman, V.A., D\u2019Ippolito, N., Uchitel, S.: Technical Report: Directed Controller Synthesis of Discrete Event Systems. CoRR, abs\/1605.09772 (2016)"},{"key":"10_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"331","DOI":"10.1007\/3-540-36577-X_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"JM Cobleigh","year":"2003","unstructured":"Cobleigh, J.M., Giannakopoulou, D., P\u0102s\u0102reanu, C.S.: Learning assumptions for compositional verification. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 331\u2013346. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/3-540-36577-X_24"},{"key":"10_CR13","doi-asserted-by":"crossref","unstructured":"De Giacomo, G., De Masellis, R., Montali, M.: Reasoning on LTL on finite traces: insensitivity to infiniteness. In: Proceedings of AAAI, pp. 1027\u20131033 (2014)","DOI":"10.1609\/aaai.v28i1.8872"},{"key":"10_CR14","first-page":"9","volume":"22","author":"N D\u2019Ippolito","year":"2013","unstructured":"D\u2019Ippolito, N., Braberman, V., Piterman, N., Uchitel, U.: Synthesising non-anomalous event-based controllers for liveness goals. ACM Tran. Softw. Eng. Methodol. 22, 9 (2013)","journal-title":"ACM Tran. Softw. Eng. Methodol."},{"key":"10_CR15","doi-asserted-by":"crossref","unstructured":"D\u2019Ippolito, N., Braberman, V., Piterman, N., Uchitel, S.: Controllability in partial and uncertain environments. In: Proceedings of ACSD, pp. 52\u201361. IEEE (2014)","DOI":"10.1109\/ACSD.2014.15"},{"key":"10_CR16","doi-asserted-by":"crossref","unstructured":"Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Property specification patterns for finite-state verification. In: Proceedings of FMSP, pp. 7\u201315. ACM (1998)","DOI":"10.1145\/298595.298598"},{"key":"10_CR17","doi-asserted-by":"crossref","unstructured":"Giannakopoulou, D., Pasareanu, C.S., Barringer, H.: Assumption generation for software component verification. In: Proceedings of ASE, pp. 3\u201312. IEEE (2002)","DOI":"10.1109\/ASE.2002.1114984"},{"issue":"3","key":"10_CR18","doi-asserted-by":"crossref","first-page":"297","DOI":"10.1007\/s10515-005-2641-y","volume":"12","author":"D Giannakopoulou","year":"2005","unstructured":"Giannakopoulou, D., P\u0103s\u0103reanu, C.S., Barringer, H.: Component verification with automatically generated assumptions. J. Autom. Softw. Eng. 12(3), 297\u2013320 (2005)","journal-title":"J. Autom. Softw. Eng."},{"issue":"4","key":"10_CR19","doi-asserted-by":"crossref","first-page":"596","DOI":"10.1145\/69575.69577","volume":"5","author":"CB Jones","year":"1983","unstructured":"Jones, C.B.: Tentative steps toward a development method for interfering programs. ACM Trans. Program. Lang. Syst. 5(4), 596\u2013619 (1983)","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"7","key":"10_CR20","doi-asserted-by":"crossref","first-page":"371","DOI":"10.1145\/360248.360251","volume":"19","author":"RM Keller","year":"1976","unstructured":"Keller, R.M.: Formal verification of parallel programs. Commun. ACM 19(7), 371\u2013384 (1976)","journal-title":"Commun. ACM"},{"key":"10_CR21","doi-asserted-by":"crossref","unstructured":"Larsen, K.G., Thomsen, B.: A modal process logic. In: Proceedings of LICS, pp. 203\u2013210. IEEE (1988)","DOI":"10.1109\/LICS.1988.5119"},{"key":"10_CR22","series-title":"Springer Books on Professional Computing Series","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-4718-0","volume-title":"Taming the Tiger: Software Engineering and Software Economics","author":"LS Levy","year":"1987","unstructured":"Levy, L.S.: Taming the Tiger: Software Engineering and Software Economics. Springer Books on Professional Computing Series. Springer-Verlag, New York (1987). https:\/\/doi.org\/10.1007\/978-1-4612-4718-0"},{"key":"10_CR23","doi-asserted-by":"crossref","unstructured":"Li, W., Dworkin, L., Seshia, S.A.: Mining assumptions for synthesis. In: Proceedings of ACM\/IEEE MEMPCODE, pp. 43\u201350 (2011)","DOI":"10.1109\/MEMCOD.2011.5970509"},{"key":"10_CR24","doi-asserted-by":"crossref","unstructured":"Lorenzoli, D., Mariani, L., Pezz\u00e8, M.: Automatic generation of software behavioral models. In: Proceedings of ICSE, pp. 501\u2013510 (2008)","DOI":"10.1145\/1368088.1368157"},{"key":"10_CR25","volume-title":"State Models and Java Programs","author":"J Magee","year":"1999","unstructured":"Magee, J., Kramer, J.: State Models and Java Programs. Wiley, New York (1999)"},{"key":"10_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"531","DOI":"10.1007\/978-3-319-48989-6_32","volume-title":"FM 2016: Formal Methods","author":"C Menghi","year":"2016","unstructured":"Menghi, C., Spoletini, P., Ghezzi, C.: Dealing with incompleteness in automata-based model checking. In: Fitzgerald, J., Heitmeyer, C., Gnesi, S., Philippou, A. (eds.) FM 2016. LNCS, vol. 9995, pp. 531\u2013550. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-48989-6_32"},{"key":"10_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"112","DOI":"10.1007\/978-3-319-54045-0_9","volume-title":"Requirements Engineering: Foundation for Software Quality","author":"C Menghi","year":"2017","unstructured":"Menghi, C., Spoletini, P., Ghezzi, C.: Integrating goal model analysis with iterative design. In: Gr\u00fcnbacher, P., Perini, A. (eds.) REFSQ 2017. LNCS, vol. 10153, pp. 112\u2013128. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-54045-0_9"},{"key":"10_CR28","unstructured":"Nivoit, J.-B.: Issues in strategic management of large-scale software product line development. Master\u2019s thesis, MIT, USA (2013)"},{"key":"10_CR29","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"106","DOI":"10.1007\/978-3-540-30106-6_11","volume-title":"Artificial Intelligence: Methodology, Systems, and Applications","author":"M Pistore","year":"2004","unstructured":"Pistore, M., Barbon, F., Bertoli, P., Shaparau, D., Traverso, P.: Planning and monitoring web service composition. In: Bussler, C., Fensel, D. (eds.) AIMSA 2004. LNCS (LNAI), vol. 3192, pp. 106\u2013115. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-30106-6_11"},{"key":"10_CR30","series-title":"NATO ASI Series","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/978-3-642-82453-1_5","volume-title":"Logics and Models of Concurrent Systems","author":"A Pnueli","year":"1985","unstructured":"Pnueli, A.: In transition from global to modular temporal reasoning about programs. In: Apt, K.R. (ed.) Logics and Models of Concurrent Systems. NATO ASI Series, pp. 123\u2013144. Springer-Verlag, New York Inc (1985). https:\/\/doi.org\/10.1007\/978-3-642-82453-1_5"},{"key":"10_CR31","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: Proceedings of POPL, pp. 179\u2013190. ACM (1989)","DOI":"10.1145\/75277.75293"},{"key":"10_CR32","doi-asserted-by":"crossref","unstructured":"Pretschner, A., Broy, M., Kruger, I.H., Stauner, T.: Software engineering for automotive systems: a roadmap. In: Proceedings of FOSE, pp. 55\u201371. IEEE Computer Society (2007)","DOI":"10.1109\/FOSE.2007.22"},{"key":"10_CR33","doi-asserted-by":"crossref","DOI":"10.1093\/oso\/9780198538455.001.0001","volume-title":"Features and Fluents (Vol. 1): The Representation of Knowledge about Dynamical Systems","author":"E Sandewall","year":"1995","unstructured":"Sandewall, E.: Features and Fluents (Vol. 1): The Representation of Knowledge about Dynamical Systems. Oxford University Press Inc, New York (1995)"},{"key":"10_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"403","DOI":"10.1007\/978-3-642-32759-9_33","volume-title":"FM 2012: Formal Methods","author":"GE Sibay","year":"2012","unstructured":"Sibay, G.E., Uchitel, S., Braberman, V., Kramer, J.: Distribution of modal transition systems. In: Giannakopoulou, D., M\u00e9ry, D. (eds.) FM 2012. LNCS, vol. 7436, pp. 403\u2013417. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-32759-9_33"},{"key":"10_CR35","unstructured":"Software Measurement Services Ltd. \u201csmall project\u201d, \u201cmedium-size project\u201d, and \u201clarge project\u201d: What do these terms mean? (2004). http:\/\/www.totalmetrics.com\/function-points-downloads\/Function-Point-Scale-Project-Size.pdf"},{"key":"10_CR36","unstructured":"Solar-Lezama, A.: Program synthesis by sketching. Ph.D. thesis. University of California, Berkeley (2008)"},{"issue":"3","key":"10_CR37","doi-asserted-by":"crossref","first-page":"384","DOI":"10.1109\/TSE.2008.107","volume":"35","author":"S Uchitel","year":"2009","unstructured":"Uchitel, S., Brunet, G., Chechik, M.: Synthesis of partial behavior models from properties and scenarios. IEEE Trans.Softw. Eng. 35(3), 384\u2013406 (2009)","journal-title":"IEEE Trans.Softw. Eng."}],"container-title":["Lecture Notes in Computer Science","Fundamental Approaches to Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-89363-1_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,7,5]],"date-time":"2024-07-05T17:50:50Z","timestamp":1720201850000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-89363-1_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319893624","9783319893631"],"references-count":37,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-89363-1_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018]]}}}