{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,10]],"date-time":"2024-09-10T17:22:51Z","timestamp":1725988971210},"publisher-location":"Cham","reference-count":22,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030002435"},{"type":"electronic","value":"9783030002442"}],"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:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-030-00244-2_9","type":"book-chapter","created":{"date-parts":[[2018,8,30]],"date-time":"2018-08-30T04:12:38Z","timestamp":1535602358000},"page":"131-146","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Virtual Integration for Pattern-Based Contracts with the Kind2 Model Checker"],"prefix":"10.1007","author":[{"given":"Jan Steffen","family":"Becker","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2018,8,30]]},"reference":[{"key":"9_CR1","unstructured":"Becker, J.S.: Analyzing consistency of formal requirements. In: Automated Verification of Critical Systems (AVOCS 2018) (2018)"},{"key":"9_CR2","unstructured":"Becker, J.S., et al.: Interoperable toolchain for requirements-driven model-based development. In: ERTS 2018 (2018)"},{"issue":"3","key":"9_CR3","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1049\/iet-sen.2009.0011","volume":"4","author":"S Bensalem","year":"2010","unstructured":"Bensalem, S., Bozga, M., Nguyen, T.H., Sifakis, J.: Compositional verification for component-based systems and application. IET Software 4(3), 181\u2013193 (2010)","journal-title":"IET Software"},{"key":"9_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"64","DOI":"10.1007\/978-3-540-88387-6_7","volume-title":"Automated Technology for Verification and Analysis","author":"S Bensalem","year":"2008","unstructured":"Bensalem, S., Bozga, M., Sifakis, J., Nguyen, T.-H.: Compositional verification for component-based systems and application. In: Cha, S.S., Choi, J.-Y., Kim, M., Lee, I., Viswanathan, M. (eds.) ATVA 2008. LNCS, vol. 5311, pp. 64\u201379. Springer, Heidelberg (2008). \nhttps:\/\/doi.org\/10.1007\/978-3-540-88387-6_7"},{"issue":"2\u20133","key":"9_CR5","doi-asserted-by":"publisher","first-page":"124","DOI":"10.1561\/1000000053","volume":"12","author":"A Benveniste","year":"2018","unstructured":"Benveniste, A.: Contracts for system design. Found. Trends Electron. Design Autom. 12(2\u20133), 124\u2013400 (2018)","journal-title":"Found. Trends Electron. Design Autom."},{"key":"9_CR6","unstructured":"Bienm\u00fcller, T., Teige, T., Eggers, A., Stasch, M.: Modeling requirements for quantitative consistency analysis and automatic test case generation. In: FM&MDD 2016. Computing Science Technical report Series, vol. CS-TR-1503. Newcastle University (2016)"},{"key":"9_CR7","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","author":"AR Bradley","year":"2011","unstructured":"Bradley, A.R.: SAT-based model checking without unrolling. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 70\u201387. Springer, Heidelberg (2011). \nhttps:\/\/doi.org\/10.1007\/978-3-642-18275-4_7"},{"key":"9_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"308","DOI":"10.1007\/978-3-319-19249-9_20","volume-title":"FM 2015: Formal Methods","author":"G Brat","year":"2015","unstructured":"Brat, G., Bushnell, D., Davies, M., Giannakopoulou, D., Howar, F., Kahsai, T.: Verifying the safety of a flight-critical system. In: Bj\u00f8rner, N., de Boer, F. (eds.) FM 2015. LNCS, vol. 9109, pp. 308\u2013324. Springer, Cham (2015). \nhttps:\/\/doi.org\/10.1007\/978-3-319-19249-9_20"},{"key":"9_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"347","DOI":"10.1007\/978-3-319-41591-8_24","volume-title":"Software Engineering and Formal Methods","author":"A Champion","year":"2016","unstructured":"Champion, A., Gurfinkel, A., Kahsai, T., Tinelli, C.: CoCoSpec: a mode-aware contract language for reactive systems. In: De Nicola, R., K\u00fchn, E. (eds.) SEFM 2016. LNCS, vol. 9763, pp. 347\u2013366. Springer, Cham (2016). \nhttps:\/\/doi.org\/10.1007\/978-3-319-41591-8_24"},{"key":"9_CR10","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Dorigatti, M., Tonetta, S.: OCRA: a tool for checking the refinement of temporal contracts. In: Proceedings of the 28th IEEE\/ACM International Conference on Automated Software Engineering, pp. 702\u2013705. IEEE Press (2013)","DOI":"10.1109\/ASE.2013.6693137"},{"key":"9_CR11","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":"NASA Formal Methods","author":"D Cofer","year":"2012","unstructured":"Cofer, D., Gacek, A., Miller, S., Whalen, M.W., LaValley, B., Sha, L.: Compositional verification of architectural models. In: Goodloe, A.E., Person, S. (eds.) NFM 2012. LNCS, vol. 7226, pp. 126\u2013140. Springer, Heidelberg (2012). \nhttps:\/\/doi.org\/10.1007\/978-3-642-28891-3_13"},{"key":"9_CR12","doi-asserted-by":"crossref","unstructured":"Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Patterns in property specifications for finite-state verification. In: Proceedings of the 21st International Conference on Software Engineering, pp. 411\u2013420. ACM (1999)","DOI":"10.1145\/302405.302672"},{"key":"9_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1007\/978-3-319-10702-8_11","volume-title":"Formal Methods for Industrial Critical Systems","author":"C Ellen","year":"2014","unstructured":"Ellen, C., Sieverding, S., Hungar, H.: Detecting consistencies and inconsistencies of pattern-based functional requirements. In: Lang, F., Flammini, F. (eds.) FMICS 2014. LNCS, vol. 8718, pp. 155\u2013169. Springer, Cham (2014). \nhttps:\/\/doi.org\/10.1007\/978-3-319-10702-8_11"},{"key":"9_CR14","doi-asserted-by":"crossref","unstructured":"Filipovikj, P., Jagerfield, T., Nyberg, M., Rodriguez-Navas, G., Seceleanu, C.: Integrating pattern-based formal requirements specification in an industrial tool-chain. In: 2016 IEEE 40th Annual Computer Software and Applications Conference (COMPSAC), vol. 2, pp. 167\u2013173. IEEE (2016)","DOI":"10.1109\/COMPSAC.2016.140"},{"key":"9_CR15","unstructured":"Gezgin, T., Oertel, M., Weber, R.: Multi-aspect virtual integration approach for real-time and safety properties. In: International Workshop on Design and Implementation of Formal Tools and Systems (DIFTS 2014). IEEE, October 2014"},{"key":"9_CR16","unstructured":"Jahier, E., Raymond, P., Halbwachs, N.: The Lustre V6 Reference Manual. IMAG, December 2016"},{"key":"9_CR17","unstructured":"Jeannet, B., Gaucher, F.: Debugging embedded systems requirements with stimulus: an automotive case-study. In: 8th European Congress on Embedded Real Time Software and Systems (ERTS 2016) (2016)"},{"key":"9_CR18","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 Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). \nhttps:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"9_CR19","unstructured":"Project TIMMO: TIMMO Partners: TADL: Timing augmented description language version 2. Deliverable d6, The TIMMO Consortium, October 2009"},{"key":"9_CR20","unstructured":"Reinkemeier, P., Stierand, I., Rehkop, P., Henkler, S.: A pattern-based requirement specification language: mapping automotive specific timing requirements. In: Software Engineering (Workshops), vol. 184, pp. 99\u2013108 (2011)"},{"key":"9_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1007\/3-540-40922-X_8","volume-title":"Formal Methods in Computer-Aided Design","author":"M Sheeran","year":"2000","unstructured":"Sheeran, M., Singh, S., St\u00e5lmarck, G.: Checking safety properties using induction and a SAT-Solver. In: Hunt, W.A., Johnson, S.D. (eds.) FMCAD 2000. LNCS, vol. 1954, pp. 127\u2013144. Springer, Heidelberg (2000). \nhttps:\/\/doi.org\/10.1007\/3-540-40922-X_8"},{"key":"9_CR22","unstructured":"Teige, T.: Simplified Universal Pattern Syntax and Semantics. BTC Embedded Systems, June 2017. Confidential"}],"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-030-00244-2_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2018,8,30]],"date-time":"2018-08-30T04:20:13Z","timestamp":1535602813000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-00244-2_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783030002435","9783030002442"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-00244-2_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]}}}