{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T07:23:58Z","timestamp":1770276238296,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540887096","type":"print"},{"value":"9783540887102","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2008]]},"DOI":"10.1007\/978-3-540-88710-2_23","type":"book-chapter","created":{"date-parts":[[2008,10,17]],"date-time":"2008-10-17T13:54:03Z","timestamp":1224251643000},"page":"286-300","source":"Crossref","is-referenced-by-count":8,"title":["A Property-Driven Approach to Formal Verification of Process Models"],"prefix":"10.1007","author":[{"given":"Beno\u00eet","family":"Combemale","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xavier","family":"Cr\u00e9gut","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pierre-Lo\u00efc","family":"Garoche","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xavier","family":"Thirioux","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Francois","family":"Vernadat","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"23_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"128","DOI":"10.1007\/978-3-540-24756-2_8","volume-title":"4th International Conference on Integrated Formal Methods (IFM)","author":"S. Chaki","year":"2004","unstructured":"Chaki, S., Clarke, E.M., Ouaknine, J., Sharygina, N., Sinha, N.: State\/event-based software model checking. In: Boiten, E.A., Derrick, J., Smith, G.P. (eds.) IFM 2004. LNCS, vol.\u00a02999, pp. 128\u2013147. Springer, Heidelberg (2004)"},{"key":"23_CR2","unstructured":"Object Management Group, Inc.: Software Process Engineering Metamodel (SPEM) 2.0 Specification, Final Adopted Specification (2007)"},{"key":"23_CR3","volume-title":"14th APSEC","author":"R. Bendraou","year":"2007","unstructured":"Bendraou, R., Combemale, B., Cr\u00e9gut, X., Gervais, M.P.: Definition of an Executable SPEM2.0. In: 14th APSEC, Japan. IEEE Computer Society, Los Alamitos (2007)"},{"key":"23_CR4","doi-asserted-by":"crossref","unstructured":"Cousot, P.: Methods and logics for proving programs. In: Handbook of Theoretical Computer Science, Volume B: Formal Models and Sematics (B), 841\u2013994 (1990)","DOI":"10.1016\/B978-0-444-88074-1.50020-2"},{"key":"23_CR5","unstructured":"Object Management Group, Inc.: UML Object Constraint Language (OCL) 2.0 Specification, Final Adopted Specification (2003)"},{"key":"23_CR6","volume-title":"The Object Constraint Language: Getting Your Models Ready for MDA","author":"J. Warmer","year":"2003","unstructured":"Warmer, J., Kleppe, A.: The Object Constraint Language: Getting Your Models Ready for MDA. Addison-Wesley Longman Publishing Co., Inc, Amsterdam (2003)"},{"key":"23_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"265","DOI":"10.1007\/3-540-40011-7_19","volume-title":"UML 2000 - The Unified Modeling Language. Advancing the Standard","author":"M. Richters","year":"2000","unstructured":"Richters, M., Gogolla, M.: Validating UML models and OCL constraints. In: Evans, A., Kent, S., Selic, B. (eds.) UML 2000. LNCS, vol.\u00a01939, pp. 265\u2013277. Springer, Heidelberg (2000)"},{"key":"23_CR8","unstructured":"Combemale, B., Rougemaille, S., Cr\u00e9gut, X., Migeon, F., Pantel, M., Maurel, C., Coulette, B.: Towards a rigorous metamodeling. In: 2nd International Workshop on Model-Driven Enterprise Information Systems, INSTICC (2006)"},{"key":"23_CR9","unstructured":"Combemale, B., Cr\u00e9gut, X., Berthomieu, B., Vernadat, F.: SimplePDL2Tina: Mise en oeuvre d\u2019une Validation de Modede Processus. In: 3ieme journ\u00e9es sur l\u2019Ing\u00e9nierie Dirig\u00e9e par les Mod\u00e9les (IDM), Toulouse, France (2007)"},{"key":"23_CR10","unstructured":"Ziemann, P., Gogolla, M.: An extension of OCL with temporal logic. In: Critical Systems Development with UML \u2013 Proceedings of the UML 2002 workshop, vol.\u00a0TUM-I0208, pp. 53\u201362 (2002)"},{"key":"23_CR11","doi-asserted-by":"publisher","first-page":"2741","DOI":"10.1080\/00207540412331312688","volume":"42","author":"B. Berthomieu","year":"2004","unstructured":"Berthomieu, B., Ribet, P.O., Vernadat, F.: The tool TINA \u2013 construction of abstract state spaces for Petri nets and time Petri nets. International Journal of Production Research\u00a042, 2741\u20132756 (2004)","journal-title":"International Journal of Production Research"},{"key":"23_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"156","DOI":"10.1007\/3-540-46852-8_12","volume-title":"\u00abUML\u00bb \u201999 - The Unified Modeling Language. Beyond the Standard","author":"M. Richters","year":"1999","unstructured":"Richters, M., Gogolla, M.: A metamodel for OCL. In: France, R.B., Rumpe, B. (eds.) UML 1999. LNCS, vol.\u00a01723, pp. 156\u2013171. Springer, Heidelberg (1999)"},{"key":"23_CR13","unstructured":"Object Management Group, Inc.: Meta Object Facility (MOF) 2.0 Core Specification, Final Adopted Specification (2006)"},{"key":"23_CR14","unstructured":"Berthomieu, B., Vernadat, F.: R\u00e9seaux de Petri temporels : m\u00e9thodes d\u2019analyse et v\u00e9rification avec TINA. Trait\u00e9 IC2 (2006)"},{"key":"23_CR15","doi-asserted-by":"crossref","unstructured":"Jouault, F., Kurtev, I.: Transforming models with ATL. In: Proceedings of the Model Transformations in Practice Workshop at MoDELS, Montego Bay, Jamaica (2005)","DOI":"10.1007\/11663430_14"},{"key":"23_CR16","unstructured":"Jouault, F.: Loosely Coupled Traceability for ATL. In: Proceedings of the European Conference on Model Driven Architecture (ECMDA) workshop on traceability (2005)"},{"key":"23_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1007\/11581741_10","volume-title":"Model Driven Architecture \u2013 Foundations and Applications","author":"K. Chen","year":"2005","unstructured":"Chen, K., Sztipanovits, J., Abdelwalhed, S., Jackson, E.: Semantic anchoring with model transformations. In: Hartman, A., Kreische, D. (eds.) ECMDA-FA 2005. LNCS, vol.\u00a03748, pp. 115\u2013129. Springer, Heidelberg (2005)"},{"key":"23_CR18","doi-asserted-by":"crossref","unstructured":"Gurevich, Y.: The abstract state machine paradigm: What is in and what is out. In: Ershov Memorial Conference (2001)","DOI":"10.1007\/3-540-45575-2_3"},{"key":"23_CR19","unstructured":"Agrawal, A., Karsai, G., Kalmar, Z., Neema, S., Shi, F., Vizhanyo, A.: The design of a language for model transformations. Technical report, Institute for Software Integrated Systems, Vanderbilt University, Nashville, USA (2005)"},{"key":"23_CR20","unstructured":"Clark, T., Evans, A., Sammut, P., Willans, J.: Applied metamodelling - a foundation for language driven development. version 0.1 (2004)"},{"key":"23_CR21","unstructured":"Flake, S.: Temporal OCL extensions for specification of real-time constraints. In: SVERTS at UML 2003, San Francisco, CA, USA (2003)"},{"key":"23_CR22","doi-asserted-by":"crossref","unstructured":"Flake, S., Mueller, W.: Formal semantics of static and temporal state-oriented OCL constraints. Journal on Software and System Modeling (SoSyM)\u00a02 (2003)","DOI":"10.1007\/s10270-003-0026-x"},{"key":"23_CR23","first-page":"390","volume-title":"International Symposium of Formal Methods Europe (FME) - Getting IT Right","author":"M.V. Cengarle","year":"2002","unstructured":"Cengarle, M.V., Knapp, A.: Towards OCL\/RT. In: International Symposium of Formal Methods Europe (FME) - Getting IT Right, pp. 390\u2013409. Springer, London (2002)"},{"key":"23_CR24","unstructured":"Distefano, D., Katoen, J.P., Rensink, A.: Towards model checking OCL. In: ECOOP Workshop on Dening a Precise Semantics for UML (2000)"},{"key":"23_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"203","DOI":"10.1007\/3-540-45923-5_14","volume-title":"Fundamental Approaches to Software Engineering","author":"J.C. Bradfield","year":"2002","unstructured":"Bradfield, J.C., Filipe, J.K., Stevens, P.: Enriching OCL using observational mu-calculus. In: Kutsche, R.-D., Weber, H. (eds.) FASE 2002. LNCS, vol.\u00a02306, pp. 203\u2013217. Springer, Heidelberg (2002)"},{"key":"23_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/11880240_8","volume-title":"Model Driven Engineering Languages and Systems","author":"P.A. Muller","year":"2006","unstructured":"Muller, P.A., Fleurey, F., Fondement, F., Hassenforder, M., Schneckenburger, R., G\u00e9rard, S., J\u00e9z\u00e9quel, J.M.: Model-driven analysis and synthesis of concrete syntax. In: Nierstrasz, O., Whittle, J., Harel, D., Reggio, G. (eds.) MoDELS 2006. LNCS, vol.\u00a04199. Springer, Heidelberg (2006)"},{"key":"23_CR27","doi-asserted-by":"crossref","unstructured":"Jouault, F., B\u00e9zivin, J., Kurtev, I.: TCS: a DSL for the Specification of Textual Concrete Syntaxes in Model Engineering. In: GPCE (2006)","DOI":"10.1145\/1173706.1173744"}],"container-title":["Lecture Notes in Business Information Processing","Enterprise Information Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-88710-2_23","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,2]],"date-time":"2025-02-02T02:52:52Z","timestamp":1738464772000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-88710-2_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008]]},"ISBN":["9783540887096","9783540887102"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-88710-2_23","relation":{},"ISSN":["1865-1348","1865-1356"],"issn-type":[{"value":"1865-1348","type":"print"},{"value":"1865-1356","type":"electronic"}],"subject":[],"published":{"date-parts":[[2008]]}}}