{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,16]],"date-time":"2025-10-16T03:57:12Z","timestamp":1760587032349,"version":"3.40.3"},"publisher-location":"Cham","reference-count":33,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030589196"},{"type":"electronic","value":"9783030589202"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"vor","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":[[2020]]},"DOI":"10.1007\/978-3-030-58920-2_7","type":"book-chapter","created":{"date-parts":[[2020,9,3]],"date-time":"2020-09-03T19:03:31Z","timestamp":1599159811000},"page":"99-114","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Counterexample Interpretation for Contract-Based Design"],"prefix":"10.1007","author":[{"given":"Arut Prakash","family":"Kaleeswaran","sequence":"first","affiliation":[]},{"given":"Arne","family":"Nordmann","sequence":"additional","affiliation":[]},{"given":"Thomas","family":"Vogel","sequence":"additional","affiliation":[]},{"given":"Lars","family":"Grunske","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2020,9,4]]},"reference":[{"key":"7_CR1","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"key":"7_CR2","unstructured":"Barbon, G., Leroy, V., Salaun, G.: Debugging of behavioural models using counterexample analysis. IEEE Trans. Softw. Eng. 1\u201314 (2019). https:\/\/ieeexplore.ieee.org\/abstract\/document\/8708934"},{"key":"7_CR3","unstructured":"Benveniste, A., Caillaud, B., Passerone, R.: A generic model of contracts for embedded systems. CoRR abs\/0706.1456 (2007)"},{"issue":"4","key":"7_CR4","first-page":"19","volume":"174","author":"L van den Berg","year":"2007","unstructured":"van den Berg, L., Strooper, P.A., Johnston, W.: An automated approach for the interpretation of counter-examples. ENTCS 174(4), 19\u201335 (2007)","journal-title":"ENTCS"},{"key":"7_CR5","doi-asserted-by":"crossref","unstructured":"Bozzano, M., Munk, P., Schweizer, M., Tonetta, S., Voz\u00e1rov\u00e1, V.: Model-based safety analysis of mode transitions. In: Proceedings of SAFECOMP (2020, in press)","DOI":"10.1007\/978-3-030-54549-9_7"},{"key":"7_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"334","DOI":"10.1007\/978-3-319-08867-9_22","volume-title":"Computer Aided Verification","author":"R Cavada","year":"2014","unstructured":"Cavada, R., et al.: The nuXmv symbolic model checker. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 334\u2013342. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_22"},{"key":"7_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1007\/3-540-45657-0_29","volume-title":"Computer Aided Verification","author":"A Cimatti","year":"2002","unstructured":"Cimatti, A., et al.: NuSMV 2: an opensource tool for symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 359\u2013364. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45657-0_29"},{"key":"7_CR8","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Tonetta, S.: A property-based proof system for contract-based design. In: 38th Euromicro Conference on Software Engineering and Advanced Applications, SEAA 2012, pp. 21\u201328 (2012)","DOI":"10.1109\/SEAA.2012.68"},{"key":"7_CR9","doi-asserted-by":"crossref","unstructured":"Clarke, E.M.: The birth of model checking. In: 25 Years of Model Checking - History, Achievements, Perspectives, pp. 1\u201326 (2008)","DOI":"10.1007\/978-3-540-69850-0_1"},{"issue":"1","key":"7_CR10","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1023\/A:1008615614281","volume":"10","author":"EM Clarke","year":"1997","unstructured":"Clarke, E.M., Grumberg, O., Hamaguchi, K.: Another look at LTL model checking. Formal Methods Syst. Des. 10(1), 47\u201371 (1997). https:\/\/doi.org\/10.1023\/A:1008615614281","journal-title":"Formal Methods Syst. Des."},{"key":"7_CR11","doi-asserted-by":"publisher","DOI":"10.1016\/B978-044450813-3\/50026-6","volume-title":"Model Checking","author":"EM Clarke","year":"2001","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (2001)"},{"issue":"4","key":"7_CR12","doi-asserted-by":"publisher","first-page":"626","DOI":"10.1145\/242223.242257","volume":"28","author":"EM Clarke","year":"1996","unstructured":"Clarke, E.M., Wing, J.M.: Formal methods: state of the art and future directions. ACM Comput. Surv. 28(4), 626\u2013643 (1996)","journal-title":"ACM Comput. Surv."},{"key":"7_CR13","doi-asserted-by":"crossref","unstructured":"Crapo, A.W., Moitra, A.: Using OWL ontologies as a domain-specific language for capturing requirements for formal analysis and test case generation. In: 13th IEEE International Conference on Semantic Computing, ICSC, pp. 361\u2013366 (2019)","DOI":"10.1109\/ICOSC.2019.8665630"},{"issue":"3","key":"7_CR14","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1016\/0164-1212(93)90029-W","volume":"21","author":"P Fenelon","year":"1993","unstructured":"Fenelon, P., McDermid, J.A.: An integrated tool set for software safety analysis. J. Syst. Softw. 21(3), 279\u2013290 (1993)","journal-title":"J. Syst. Softw."},{"key":"7_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1007\/11921998_17","volume-title":"Quality of Software Architectures","author":"L Grunske","year":"2006","unstructured":"Grunske, L.: Towards an integration of standard component-based safety evaluation techniques with SaveCCM. In: Hofmeister, C., Crnkovic, I., Reussner, R. (eds.) QoSA 2006. LNCS, vol. 4214, pp. 199\u2013213. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11921998_17"},{"issue":"2","key":"7_CR16","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1007\/s10009-004-0146-9","volume":"6","author":"HS Jin","year":"2004","unstructured":"Jin, H.S., Ravi, K., Somenzi, F.: Fate and free will in error traces. Int. J. Softw. Tools Technol. Transf. 6(2), 102\u2013116 (2004). https:\/\/doi.org\/10.1007\/s10009-004-0146-9","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"7_CR17","first-page":"66","volume":"4","author":"B Kaiser","year":"2015","unstructured":"Kaiser, B., Weber, R., Oertel, M., B\u00f6de, E., Nejad, B.M., Zander, J.: Contract-based design of embedded systems integrating nominal behavior and safety. CSIMQ 4, 66\u201391 (2015)","journal-title":"CSIMQ"},{"key":"7_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1007\/978-3-030-32872-6_4","volume-title":"Model-Based Safety and Assessment","author":"AP Kaleeswaran","year":"2019","unstructured":"Kaleeswaran, A.P., Munk, P., Sarkic, S., Vogel, T., Nordmann, A.: A domain specific language to support HAZOP studies of SysML models. In: Papadopoulos, Y., Aslansefat, K., Katsaros, P., Bozzano, M. (eds.) IMBSA 2019. LNCS, vol. 11842, pp. 47\u201362. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-32872-6_4"},{"key":"7_CR19","unstructured":"Kaleeswaran, A.P., Nordmann, A., ul Mehdi, A.: Towards integrating ontologies into verification for autonomous driving. In: ISWC 2019 Satellite Tracks (Posters & Demonstrations, Industry, and Outrageous Ideas), pp. 319\u2013320 (2019)"},{"key":"7_CR20","doi-asserted-by":"crossref","unstructured":"Langenfeld, V., Dietsch, D., Westphal, B., Hoenicke, J., Post, A.: Scalable analysis of real-time requirements. In: 27th IEEE International Requirements Engineering Conference, RE, pp. 234\u2013244 (2019)","DOI":"10.1109\/RE.2019.00033"},{"key":"7_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1007\/978-3-642-31759-0_5","volume-title":"Model Checking Software","author":"S Leue","year":"2012","unstructured":"Leue, S., Tabaei Befrouei, M.: Counterexample explanation by anomaly detection. In: Donaldson, A., Parker, D. (eds.) SPIN 2012. LNCS, vol. 7385, pp. 24\u201342. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31759-0_5"},{"key":"7_CR22","unstructured":"Marcantonio, D., Tonetta, S.: Redundant Sensors (2014). https:\/\/es-static.fbk.eu\/tools\/ocra\/download\/RedundantSensors.pdf"},{"issue":"3","key":"7_CR23","doi-asserted-by":"publisher","first-page":"341","DOI":"10.1007\/s00766-019-00316-x","volume":"24","author":"A Moitra","year":"2019","unstructured":"Moitra, A., et al.: Automating requirements analysis and test case generation. Requir. Eng. 24(3), 341\u2013364 (2019). https:\/\/doi.org\/10.1007\/s00766-019-00316-x","journal-title":"Requir. Eng."},{"key":"7_CR24","doi-asserted-by":"crossref","unstructured":"Munk, P., et al.: Semi-automatic safety analysis and optimization. In: 55th ACM\/ESDA\/IEEE Design Automation Conference (DAC) (2018)","DOI":"10.1109\/DAC.2018.8465805"},{"key":"7_CR25","doi-asserted-by":"publisher","first-page":"889","DOI":"10.1007\/s10270-020-00782-w","volume":"19","author":"P Munk","year":"2020","unstructured":"Munk, P., Nordmann, A.: Model-based safety assessment with SysML and component fault trees: application and lessons learned. Softw. Syst. Model. 19, 889\u2013910 (2020). https:\/\/doi.org\/10.1007\/s10270-020-00782-w","journal-title":"Softw. Syst. Model."},{"key":"7_CR26","series-title":"Lecture Notes in Business Information Processing","doi-asserted-by":"publisher","first-page":"515","DOI":"10.1007\/978-3-319-42887-1_41","volume-title":"Business Process Management Workshops","author":"FU Muram","year":"2016","unstructured":"Muram, F.U., Tran, H., Zdun, U.: Counterexample analysis for supporting containment checking of business process models. In: Reichert, M., Reijers, H. (eds.) BPM 2015. LNBIP, vol. 256, pp. 515\u2013528. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-42887-1_41"},{"issue":"3\u20134","key":"7_CR27","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1007\/s11334-019-00339-1","volume":"15","author":"M Narizzano","year":"2019","unstructured":"Narizzano, M., Pulina, L., Tacchella, A., Vuotto, S.: Property specification patterns at work: verification and inconsistency explanation. Innov. Syst. Softw. Eng. 15(3\u20134), 307\u2013323 (2019). https:\/\/doi.org\/10.1007\/s11334-019-00339-1","journal-title":"Innov. Syst. Softw. Eng."},{"key":"7_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"474","DOI":"10.1007\/978-3-540-27863-4_26","volume-title":"Integration of Software Specification Techniques for Applications in Engineering","author":"F Ortmeier","year":"2004","unstructured":"Ortmeier, F., Thums, A., Schellhorn, G., Reif, W.: Combining formal methods and safety analysis \u2013 the ForMoSA approach. In: Ehrig, H., et al. (eds.) Integration of Software Specification Techniques for Applications in Engineering. LNCS, vol. 3147, pp. 474\u2013493. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-27863-4_26"},{"key":"7_CR29","doi-asserted-by":"crossref","unstructured":"Pakonen, A., Buzhinsky, I., Vyatkin, V.: Counterexample visualization and explanation for function block diagrams. In: INDIN, pp. 747\u2013753 (2018)","DOI":"10.1109\/INDIN.2018.8472025"},{"issue":"3","key":"7_CR30","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1016\/S0951-8320(00)00076-4","volume":"71","author":"Y Papadopoulos","year":"2001","unstructured":"Papadopoulos, Y., McDermid, J., Sasse, R., Heiner, G.: Analysis and synthesis of the behaviour of complex programmable electronic systems in conditions of failure. Reliab. Eng. Syst. Saf. 71(3), 229\u2013247 (2001)","journal-title":"Reliab. Eng. Syst. Saf."},{"key":"7_CR31","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science, pp. 46\u201357 (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"7_CR32","doi-asserted-by":"crossref","unstructured":"Ratiu, D., Gario, M., Schoenhaar, H.: FASTEN: an open extensible framework to experiment with formal specification approaches: using language engineering to develop a multi-paradigm specification environment for NuSMV. In: FormaliSE@ICSE, pp. 41\u201350. IEEE\/ACM (2019)","DOI":"10.1109\/FormaliSE.2019.00013"},{"key":"7_CR33","doi-asserted-by":"publisher","first-page":"64","DOI":"10.1016\/j.ress.2014.10.025","volume":"135","author":"S Sharvia","year":"2015","unstructured":"Sharvia, S., Papadopoulos, Y.: Integrating model checking with hip-hops in model-based safety analysis. Reliab. Eng. Syst. Saf. 135, 64\u201380 (2015)","journal-title":"Reliab. Eng. Syst. Saf."}],"container-title":["Lecture Notes in Computer Science","Model-Based Safety and Assessment"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-58920-2_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,24]],"date-time":"2021-04-24T09:56:17Z","timestamp":1619258177000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-58920-2_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030589196","9783030589202"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-58920-2_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"4 September 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"IMBSA","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Model-Based Safety and Assessment","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Lisbon","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Portugal","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"14 September 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16 September 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"imbsa2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/easyconferences.eu\/imbsa2020\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Easychair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"30","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"15","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"4","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"50% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"2","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"No","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Conference was held vertually due to COVID_19 pandemic.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}