{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,8]],"date-time":"2026-04-08T08:15:55Z","timestamp":1775636155545,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642169007","type":"print"},{"value":"9783642169014","type":"electronic"}],"license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-16901-4_38","type":"book-chapter","created":{"date-parts":[[2010,11,8]],"date-time":"2010-11-08T12:40:06Z","timestamp":1289220006000},"page":"581-596","source":"Crossref","is-referenced-by-count":34,"title":["Comparison of Model Checking Tools for Information Systems"],"prefix":"10.1007","author":[{"given":"Marc","family":"Frappier","sequence":"first","affiliation":[]},{"given":"Beno\u00eet","family":"Fraikin","sequence":"additional","affiliation":[]},{"given":"Romain","family":"Chossart","sequence":"additional","affiliation":[]},{"given":"Rapha\u00ebl","family":"Chane-Yack-Fa","sequence":"additional","affiliation":[]},{"given":"Mohammed","family":"Ouenzar","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"38_CR1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511624162","volume-title":"The B-Book: Assigning Programs to Meanings","author":"J.R. Abrial","year":"1996","unstructured":"Abrial, J.R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press, Cambridge (1996)"},{"key":"38_CR2","doi-asserted-by":"crossref","unstructured":"Augusto, J.C., Ferreira, C., Gravell, A.M., Leuschel, M., Ng, K.M.Y.: The benefits of rapid modelling for e-business system development. In: ER Workshops, pp. 17\u201328 (2003)","DOI":"10.1007\/978-3-540-39597-3_3"},{"key":"38_CR3","doi-asserted-by":"crossref","unstructured":"Aydal, E.G., Utting, M., Woodcock, J.: A comparison of state-based modelling tools for model validation. In: TOOLS-Europe 2008, Switzerland. LNBIP, vol.\u00a011, pp. 278\u2013296 (2008)","DOI":"10.1007\/978-3-540-69824-1_16"},{"key":"38_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/3-540-49059-0_14","volume-title":"Tools and Algorithms for the Construction of Analysis of Systems","author":"A. Biere","year":"1999","unstructured":"Biere, A., Clarke, E.M., Cimatti, A., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol.\u00a01579, pp. 193\u2013207. Springer, Heidelberg (1999)"},{"key":"38_CR5","first-page":"23","volume-title":"The Formal Description Technique LOTOS","author":"T. Bolognesi","year":"1989","unstructured":"Bolognesi, T., Brinksma, E.: Introduction to the ISO specification language LOTOS. In: van Eijk, P.H.J., Vissers, C.A., Diaz, M. (eds.) The Formal Description Technique LOTOS, pp. 23\u201373. Elsevier Science Publishers B.V., Amsterdam (1989)"},{"key":"38_CR6","unstructured":"Chane-Yack-Fa, R., Fraikin, B., Frappier, M., Chossard, R., Ouenzar, M.: Comparison of model checking tools for information systems. Tech. Rep.\u00a029, Universit de Sherbrooke (2010), http:\/\/pages.usherbrooke.ca\/gril\/TR\/TR-GRIL-1006-29.pdf"},{"key":"38_CR7","series-title":"Lecture Notes in Computer Science","volume-title":"Logics of Programs","author":"E.M. Clarke","year":"1981","unstructured":"Clarke, E.M., Emerson, E.A.: Synthesis of synchronization skeletons for branching time temporal logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol.\u00a0131. Springer, Heidelberg (1981)"},{"issue":"3","key":"38_CR8","doi-asserted-by":"publisher","first-page":"442","DOI":"10.1016\/j.jcss.2006.10.006","volume":"73","author":"A. Deutsch","year":"2007","unstructured":"Deutsch, A., Sui, L., Vianu, V.: Specification and verification of data-driven web applications. Journal of Computer and System Sciences\u00a073(3), 442\u2013474 (2007)","journal-title":"Journal of Computer and System Sciences"},{"issue":"1","key":"38_CR9","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1145\/4904.4999","volume":"33","author":"E.A. Emerson","year":"1986","unstructured":"Emerson, E.A., Halpern, J.Y.: \u201cSometimes\u201d and \u201cNot Never\u201d revisited: On branching versus linear time temporal logic. J. ACM\u00a033(1), 151\u2013178 (1986)","journal-title":"J. ACM"},{"key":"38_CR10","unstructured":"Garavel, H.: Compilation et vrification de programmes LOTOS. Ph.D. thesis, Universit Joseph Fourier, Grenoble (November 1989)"},{"key":"38_CR11","volume-title":"The Spin Model Checker: Primer and Reference Manual","author":"G.J. Holzmann","year":"2004","unstructured":"Holzmann, G.J.: The Spin Model Checker: Primer and Reference Manual. Addison-Wesley, Reading (2004)"},{"key":"38_CR12","volume-title":"Software Abstractions","author":"D. Jackson","year":"2006","unstructured":"Jackson, D.: Software Abstractions. MIT Press, Cambridge (2006)"},{"key":"38_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"855","DOI":"10.1007\/978-3-540-45236-2_46","volume-title":"FME 2003: Formal Methods","author":"M. Leuschel","year":"2003","unstructured":"Leuschel, M., Butler, M.: ProB: A model checker for B. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol.\u00a02805, pp. 855\u2013874. Springer, Heidelberg (2003)"},{"key":"38_CR14","unstructured":"Mateescu, R., Garavel, H.: XTL: A meta-language and tool for temporal logic model-checking. In: Proceedings of the International Workshop on Software Tools for Technology Transfer STTT 1998, Aalborg, Denmark, p. 10 (July 1998)"},{"key":"38_CR15","doi-asserted-by":"crossref","unstructured":"McMillan, K.L.: Symbolic Model Checking. Ph.D. thesis, Carnegie Mellon University (1993)","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"38_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"514","DOI":"10.1007\/978-3-540-69387-1_58","volume-title":"Computational Science \u2013 ICCS 2008","author":"S. Morimoto","year":"2008","unstructured":"Morimoto, S.: A survey of formal verification for business process modeling. In: Bubak, M., van Albada, G.D., Dongarra, J., Sloot, P.M.A. (eds.) ICCS 2008, Part II. LNCS, vol.\u00a05102, pp. 514\u2013524. Springer, Heidelberg (2008)"},{"key":"38_CR17","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":"38_CR18","volume-title":"The Theory and Practice of Concurrency","author":"B.A.W. Roscoe","year":"1998","unstructured":"Roscoe, B.A.W.: The Theory and Practice of Concurrency, 3rd edn. Prentice Hall PTR, Englewood Cliffs (1998) (amended 2005)","edition":"3"},{"key":"38_CR19","unstructured":"Spielmann, M.: Abstract state machines: Verification problems and complexity. Ph.D. thesis, Bibliothek der RWTH Aachen (2000)"},{"issue":"1","key":"38_CR20","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1016\/j.scico.2006.08.007","volume":"65","author":"W.L. Yeung","year":"2007","unstructured":"Yeung, W.L., Leung, K.R.P.H., Wang, J., Dong, W.: Modelling and model checking suspendible business processes via statechart diagrams and CSP. Science of Computer Programming\u00a065(1), 14\u201329 (2007)","journal-title":"Science of Computer Programming"}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-16901-4_38","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,6]],"date-time":"2019-06-06T00:12:24Z","timestamp":1559779944000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-16901-4_38"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642169007","9783642169014"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-16901-4_38","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010]]}}}