{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T17:10:05Z","timestamp":1760202605311,"version":"3.37.3"},"reference-count":37,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2010,2,11]],"date-time":"2010-02-11T00:00:00Z","timestamp":1265846400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Softw Syst Model"],"published-print":{"date-parts":[[2011,2]]},"DOI":"10.1007\/s10270-010-0148-x","type":"journal-article","created":{"date-parts":[[2010,2,10]],"date-time":"2010-02-10T06:46:38Z","timestamp":1265784398000},"page":"117-142","source":"Crossref","is-referenced-by-count":9,"title":["Exploring inconsistencies between modal transition systems"],"prefix":"10.1007","volume":"10","author":[{"given":"Mathieu","family":"Sassolas","sequence":"first","affiliation":[]},{"given":"Marsha","family":"Chechik","sequence":"additional","affiliation":[]},{"given":"Sebastian","family":"Uchitel","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2010,2,11]]},"reference":[{"key":"148_CR1","doi-asserted-by":"crossref","unstructured":"Brunet, G., Chechik, M., Uchitel, S.: Properties of behavioural model merging. In: Proceedings of International Conference on Formal Methods (FM\u201906). LNCS, vol. 4085, pp. 98\u2013114. Springer, Berlin (2006)","DOI":"10.1007\/11813040_8"},{"issue":"1","key":"148_CR2","doi-asserted-by":"crossref","first-page":"49","DOI":"10.1007\/s10009-002-0095-0","volume":"5","author":"T. Ball","year":"2003","unstructured":"Ball T., Podelski A., Rajamani S.: Boolean and Cartesian Abstraction for Model Checking C Programs. Int. J. Softw. Tools Technol. Transf. (STTT) 5(1), 49\u201358 (2003)","journal-title":"Int. J. Softw. Tools Technol. Transf. (STTT)"},{"key":"148_CR3","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Clarke, E.M., Giunchiglia, F., Roveri, M.: NuSMV: a new Symbolic Model Verifier. In: Proceedings of CAV\u201999. LNCS, vol. 1633, pp. 495\u2013499 (1999)","DOI":"10.1007\/3-540-48683-6_44"},{"key":"148_CR4","doi-asserted-by":"crossref","unstructured":"Chechik, M., Gurfinkel, A.: A framework for counterexample generation and exploration. Int. J. Softw. Tools Technol. Transf. (STTT) 9(5\u20136) (2007)","DOI":"10.1007\/s10009-007-0047-9"},{"key":"148_CR5","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Grumberg, O., McMillan, K.L., Zhao, X.: Efficient generation of counterexamples and witnesses in symbolic model checking. In: Proceedings of 32nd Design Automation Conference (DAC\u201995), pp. 427\u2013432 (1995)","DOI":"10.1145\/217474.217565"},{"key":"148_CR6","volume-title":"Model Checking","author":"E. Clarke","year":"1999","unstructured":"Clarke E., Grumberg O., Peled D.: Model Checking. MIT Press, Cambridge (1999)"},{"issue":"3","key":"148_CR7","doi-asserted-by":"crossref","first-page":"335","DOI":"10.1007\/s10009-002-0097-y","volume":"4","author":"F. Copty","year":"2003","unstructured":"Copty F., Irron A., Weissberg O., Kropp N., Kamhi G.: Efficient debugging in a formal verification environment. Int. J. Softw. Tools Technol. Transf. (STTT) 4(3), 335\u2013348 (2003)","journal-title":"Int. J. Softw. Tools Technol. Transf. (STTT)"},{"key":"148_CR8","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Lu, Y., Jha, S., Veith, H.: Tree-Like counterexamples in model checking. In: Proceedings of the Seventeenth Annual IEEE Symposium on Logic in Computer Science (LICS\u201902), pp. 19\u201329. IEEE Computer Society, Los Alamitos (2002)","DOI":"10.1109\/LICS.2002.1029814"},{"issue":"1","key":"148_CR9","doi-asserted-by":"crossref","first-page":"36","DOI":"10.1145\/151646.151648","volume":"15","author":"R. Cleaveland","year":"1993","unstructured":"Cleaveland R., Parrow J., Steffen B.: The concurrency workbench: a semantics based tool for the verification of concurrent systems. ACM Trans. Program. Lang. Syst. 15(1), 36\u201372 (1993)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"148_CR10","doi-asserted-by":"crossref","unstructured":"D\u2019Ippolito, N., Fishbein, D., Chechik, M., Uchitel, S.: MTSA: the modal transition system analyzer. In: Proceedings of International Conference on Automated Software Engineering (ASE\u201908), pp. 475\u2013476 (2008)","DOI":"10.1109\/ASE.2008.78"},{"key":"148_CR11","doi-asserted-by":"crossref","unstructured":"Dong, Y., Ramakrishnan, C.R., Smolka, S.A.: Evidence explorer: a tool for exploring model-checking proofs. In: Proceedings of the 15th International Conference on Computer-Aided Verification (CAV\u201903). LNCS, vol. 2725, pp. 215\u2013218 (2003)","DOI":"10.1007\/978-3-540-45069-6_22"},{"key":"148_CR12","doi-asserted-by":"crossref","unstructured":"Easterbrook, S., Chechik, M.: A framework for multi-valued reasoning over inconsistent viewpoints. In: Proceedings of International Conference on Software Engineering (ICSE\u201901), pp. 411\u2013420. IEEE Computer Society Press, Los Alamitos (2001)","DOI":"10.1109\/ICSE.2001.919114"},{"issue":"8","key":"148_CR13","doi-asserted-by":"crossref","first-page":"569","DOI":"10.1109\/32.310667","volume":"20","author":"A.C.W. Finkelstein","year":"1994","unstructured":"Finkelstein A.C.W., Gabbay D., Hunter A., Kramer J., Nuseibeh B.: Inconsistency handling in multi-perspective specifications. IEEE Trans. Softw. Eng. 20(8), 569\u2013578 (1994)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"148_CR14","doi-asserted-by":"crossref","unstructured":"Fischbein, D., Uchitel, S.: On correct and complete merging of partial behaviour models. In: Proceedings of SIGSOFT Conference on Foundations of Software Engineering (FSE\u201908), pp. 297\u2013307 (2008)","DOI":"10.1145\/1453101.1453144"},{"key":"148_CR15","doi-asserted-by":"crossref","unstructured":"Giannakopoulou, D., Magee, J.: Fluent model checking for event-based systems. In: Proceedings of the 9th Joint Meeting of the European Software Engineering Conference and ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC\/FSE\u201903), pp. 257\u2013266. ACM Press, New York (2003)","DOI":"10.1145\/940071.940106"},{"key":"148_CR16","doi-asserted-by":"crossref","unstructured":"Groce, A., Visser, W.: What went wrong: explaining counterexamples. In: Proceedings of SPIN Workshop on Model Checking of Software, pp. 121\u2013135 (2003)","DOI":"10.1007\/3-540-44829-2_8"},{"key":"148_CR17","doi-asserted-by":"crossref","first-page":"231","DOI":"10.1016\/0167-6423(87)90035-9","volume":"8","author":"D. Harel","year":"1987","unstructured":"Harel D.: StateCharts: a visual formalism for complex systems. Sci. Comp. Program. 8, 231\u2013274 (1987)","journal-title":"Sci. Comp. Program."},{"key":"148_CR18","doi-asserted-by":"crossref","unstructured":"Huth, M., Jagadeesan, R., Schmidt, D.A.: Modal transition systems: a foundation for three-valued program analysis. In: Proceedings of 10th European Symposium on Programming (ESOP\u201901). LNCS, vol. 2028, pp. 155\u2013169. Springer, Berlin (2001)","DOI":"10.1007\/3-540-45309-1_11"},{"key":"148_CR19","volume-title":"Communicating Sequential Processes","author":"C.A.R. Hoare","year":"1985","unstructured":"Hoare C.A.R.: Communicating Sequential Processes. Prentice-Hall, New York (1985)"},{"issue":"5","key":"148_CR20","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G.J. Holzmann","year":"1997","unstructured":"Holzmann G.J.: The model checker SPIN. IEEE Trans. Softw. Eng. 23(5), 279\u2013295 (1997)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"148_CR21","doi-asserted-by":"crossref","unstructured":"Huth, M., Pradhan, S.: Model-checking view-based partial specifications. Electr. Notes Theoret. Comput. Sci. 45 (2001)","DOI":"10.1016\/S1571-0661(04)80962-9"},{"issue":"7","key":"148_CR22","doi-asserted-by":"crossref","first-page":"371","DOI":"10.1145\/360248.360251","volume":"19","author":"R. Keller","year":"1976","unstructured":"Keller R.: Formal verification of parallel programs. Commun. ACM 19(7), 371\u2013384 (1976)","journal-title":"Commun. ACM"},{"issue":"2","key":"148_CR23","doi-asserted-by":"crossref","first-page":"175","DOI":"10.1007\/s10515-008-0027-7","volume":"15","author":"E. Letier","year":"2008","unstructured":"Letier E., Kramer J., Magee J., Uchitel S.: Deriving event-based transition systems from goal-oriented requirements models. J. Autom. Softw. Eng. 15(2), 175\u2013206 (2008)","journal-title":"J. Autom. Softw. Eng."},{"key":"148_CR24","doi-asserted-by":"crossref","unstructured":"Larsen, K.G., Thomsen, B.: A modal process logic. In: Proceedings of 3rd Annual Symposium on Logic in Computer Science (LICS\u201988), pp. 203\u2013210. IEEE Computer Society Press, Los Alamitos (1988)","DOI":"10.1109\/LICS.1988.5119"},{"key":"148_CR25","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-10235-3","volume-title":"A Calculus of Communicating Systems","author":"R. Milner","year":"1980","unstructured":"Milner R.: A Calculus of Communicating Systems. Springer, Berlin (1980)"},{"key":"148_CR26","volume-title":"Communicating and Mobile Systems: the Pi-Calculus","author":"R. Milner","year":"1999","unstructured":"Milner R.: Communicating and Mobile Systems: the Pi-Calculus. Cambridge University Press, Cambridge (1999)"},{"key":"148_CR27","doi-asserted-by":"crossref","unstructured":"Namjoshi, K.: Certifying model checkers. In: Proceedings of 13th International Conference on Computer-Aided Verification (CAV\u201901). LNCS, vol. 2102. Springer, Berlin (2001)","DOI":"10.1007\/3-540-44585-4_2"},{"key":"148_CR28","doi-asserted-by":"crossref","unstructured":"Nejati, S., Chechik, M.: Let\u2019s agree to disagree. In: Proceedings of 20th IEEE International Conference on Automated Software Engineering (ASE\u201905), pp. 287\u2013290. IEEE Computer Society, Los Almitos (2005)","DOI":"10.1145\/1101908.1101952"},{"issue":"2","key":"148_CR29","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1145\/514183.514186","volume":"2","author":"C. Nentwich","year":"2002","unstructured":"Nentwich C., Capra L., Emmerich W., Finkelstein A.: xlinkit: a consistency checking and smart link generation service. ACM Trans. Int. Technol. 2(2), 151\u2013185 (2002)","journal-title":"ACM Trans. Int. Technol."},{"issue":"10","key":"148_CR30","doi-asserted-by":"crossref","first-page":"760","DOI":"10.1109\/32.328995","volume":"20","author":"B. Nuseibeh","year":"1994","unstructured":"Nuseibeh B., Kramer J., Finkelstein A.: Framework for expressing the relationship between multiple views in requirements specifications. IEEE Trans. Softw. Eng. 20(10), 760\u2013773 (1994)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"148_CR31","doi-asserted-by":"crossref","unstructured":"Nejati, S., Sabetzdeh, M., Chechik, M., Easterbrook, S., Zave, P.: Matching and merging of statecharts specifications. In: Proceedings of the 29th International Conference on Software Engineering (ICSE\u201907), pp. 54\u201364 (2007)","DOI":"10.1109\/ICSE.2007.50"},{"key":"148_CR32","doi-asserted-by":"crossref","unstructured":"Roscoe, A.W., Broadfoot, P.: Tutorial on FDR and its applications. In: Proceedings of the 9th SPIN Workshop on Model Checking Software (SPIN\u201900). LNCS, vol. 1885, p. 322. Springer, Berlin (2000)","DOI":"10.1007\/10722468_18"},{"key":"148_CR33","unstructured":"Sassolas, M.: PseudoMerge: a prototype tool. http:\/\/pagesperso-systeme.lip6.fr\/Mathieu.Sassolas\/recherche\/tools\/PseudoMergePrototype.zip (2009)"},{"key":"148_CR34","doi-asserted-by":"crossref","unstructured":"Sabetzadeh, M., Easterbrook, S.M.: Analysis of inconsistency in graph-based viewpoints: a category-theoretic approach. In: Proceedings of 18th IEEE International Conference on Automated Software Engineering (ASE\u201903), pp. 12\u201321. IEEE Computer Society, Los Almitos (2003)","DOI":"10.1109\/ASE.2003.1240290"},{"key":"148_CR35","doi-asserted-by":"crossref","unstructured":"Tan, L., Cleaveland, R.: Evidence-based model checking. In: Proceedings of 14th Conference on Computer-Aided Verification (CAV\u201902). LNCS, vol. 2404, pp. 455\u2013470. Springer, Berlin (2002)","DOI":"10.1007\/3-540-45657-0_37"},{"issue":"3","key":"148_CR36","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."},{"key":"148_CR37","doi-asserted-by":"crossref","unstructured":"Uchitel, S., Chechik, M.: Merging partial behavioural models. In: Proceedings of 12th ACM SIGSOFT International Symposium on Foundations of Software Engineering (FSE\u201904), pp. 43\u201352 (2004)","DOI":"10.1145\/1029894.1029904"}],"container-title":["Software & Systems Modeling"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-010-0148-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10270-010-0148-x\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-010-0148-x","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,18]],"date-time":"2025-02-18T03:57:19Z","timestamp":1739851039000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10270-010-0148-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,2,11]]},"references-count":37,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2011,2]]}},"alternative-id":["148"],"URL":"https:\/\/doi.org\/10.1007\/s10270-010-0148-x","relation":{},"ISSN":["1619-1366","1619-1374"],"issn-type":[{"type":"print","value":"1619-1366"},{"type":"electronic","value":"1619-1374"}],"subject":[],"published":{"date-parts":[[2010,2,11]]}}}