{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,1]],"date-time":"2025-11-01T06:02:42Z","timestamp":1761976962148,"version":"build-2065373602"},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642412011"},{"type":"electronic","value":"9783642412028"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-41202-8_14","type":"book-chapter","created":{"date-parts":[[2013,10,21]],"date-time":"2013-10-21T05:11:19Z","timestamp":1382332279000},"page":"199-214","source":"Crossref","is-referenced-by-count":4,"title":["A Modular Approach for Reusing Formalisms in Verification Tools of Concurrent Systems"],"prefix":"10.1007","author":[{"given":"\u00c9tienne","family":"Andr\u00e9","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Beno\u00eet","family":"Barbot","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Cl\u00e9ment","family":"D\u00e9moulins","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lom Messan","family":"Hillah","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Francis","family":"Hulin-Hubard","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Fabrice","family":"Kordon","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alban","family":"Linard","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Laure","family":"Petrucci","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"2","key":"14_CR1","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R. Alur","year":"1994","unstructured":"Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Computer Science\u00a0126(2), 183\u2013235 (1994)","journal-title":"Theoretical Computer Science"},{"key":"14_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1007\/978-3-642-32759-9_6","volume-title":"FM 2012: Formal Methods","author":"\u00c9. Andr\u00e9","year":"2012","unstructured":"Andr\u00e9, \u00c9., Fribourg, L., K\u00fchne, U., Soulat, R.: IMITATOR\u00a02.5: A\u00a0tool for analyzing robustness in scheduling problems. In: Giannakopoulou, D., M\u00e9ry, D. (eds.) FM 2012. LNCS, vol.\u00a07436, pp. 33\u201336. Springer, Heidelberg (2012)"},{"key":"14_CR3","unstructured":"Andr\u00e9, \u00c9., Hillah, L.-M., Hulin-Hubard, F., Kordon, F., Lembachar, Y., Linard, A., Petrucci, L.: CosyVerif: An open source extensible verification environment. In: ICECCS. IEEE Computer Society (to appear, 2013)"},{"key":"14_CR4","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1016\/j.tcs.2012.04.046","volume":"449","author":"P. Baldan","year":"2012","unstructured":"Baldan, P., Bruni, A., Corradini, A., K\u00f6nig, B., Rodr\u00edguez, C., Schwoon, S.: Efficient unfolding of contextual Petri nets. Theoretical Computer Science\u00a0449, 2\u201322 (2012)","journal-title":"Theoretical Computer Science"},{"key":"14_CR5","doi-asserted-by":"crossref","unstructured":"Ballarini, P., Djafri, H., Duflot, M., Haddad, S., Pekergin, N.: HASL: An\u00a0expressive language for statistical verification of stochastic models. In: VALUETOOLS, pp. 306\u2013315 (2011)","DOI":"10.4108\/icst.valuetools.2011.245710"},{"key":"14_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"354","DOI":"10.1007\/978-3-642-14295-6_31","volume-title":"Computer Aided Verification","author":"S. Blom","year":"2010","unstructured":"Blom, S., van de Pol, J., Weber, M.: LTSmin: Distributed and symbolic reachability. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol.\u00a06174, pp. 354\u2013359. Springer, Heidelberg (2010)"},{"key":"14_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"338","DOI":"10.1007\/978-3-642-21834-7_20","volume-title":"Applications and Theory of Petri Nets","author":"M. Colange","year":"2011","unstructured":"Colange, M., Baarir, S., Kordon, F., Thierry-Mieg, Y.: Crocodile: A symbolic\/symbolic tool for the analysis of symmetric nets with bags. In: Kristensen, L.M., Petrucci, L. (eds.) PETRI NETS 2011. LNCS, vol.\u00a06709, pp. 338\u2013347. Springer, Heidelberg (2011)"},{"key":"14_CR8","unstructured":"Ferr\u00e9, S., Ridoux, O.: Logic functors: A toolbox of components for building customized and embeddable logics. Technical report, INRIA (2006), http:\/\/www.irisa.fr\/LIS\/ferre\/logfun\/doc\/ResearchReportInria0000.pdf"},{"key":"14_CR9","doi-asserted-by":"crossref","unstructured":"Haddad, S., Kordon, F., Petrucci, L., Pradat-Peyre, J.-F., Tr\u00e8ves, N.: Efficient state-based analysis by introducing bags in Petri net color domains. In: ACC 2009, pp. 5018\u20135025. Omnipress IEEE (2009)","DOI":"10.1109\/ACC.2009.5160020"},{"key":"14_CR10","doi-asserted-by":"crossref","unstructured":"Hamez, A., Hillah, L.-M., Kordon, F., Linard, A., Paviot-Adet, E., Renault, X., Thierry-Mieg, Y.: New features in CPN-AMI\u00a03: Focusing on the analysis of complex distributed systems. In: ACSD, pp. 273\u2013275. IEEE Computer Society (2006)","DOI":"10.1109\/ACSD.2006.15"},{"key":"14_CR11","doi-asserted-by":"publisher","first-page":"110","DOI":"10.1007\/s100090050008","volume":"1","author":"T.A. Henzinger","year":"1997","unstructured":"Henzinger, T.A., Ho, P.-H., Wong-Toi, H.: HyTech: A model checker for hybrid systems. Software Tools for Technology Transfer\u00a01, 110\u2013122 (1997)","journal-title":"Software Tools for Technology Transfer"},{"key":"14_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"318","DOI":"10.1007\/978-3-642-13675-7_20","volume-title":"Applications and Theory of Petri Nets","author":"L.M. Hillah","year":"2010","unstructured":"Hillah, L.M., Kordon, F., Petrucci, L., Tr\u00e8ves, N.: PNML framework: An extendable reference implementation of the Petri net markup language. In: Lilius, J., Penczek, W. (eds.) PETRI NETS 2010. LNCS, vol.\u00a06128, pp. 318\u2013327. Springer, Heidelberg (2010)"},{"key":"14_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1007\/978-3-642-29072-5_5","volume-title":"Transactions on Petri Nets and Other Models of Concurrency V","author":"S. Hong","year":"2012","unstructured":"Hong, S., Kordon, F., Paviot-Adet, E., Evangelista, S.: Computing a hierarchical static order for decision diagram-based representation from P\/T nets. In: Jensen, K., Donatelli, S., Kleijn, J. (eds.) ToPNoC 2012. LNCS, vol.\u00a06900, pp. 121\u2013140. Springer, Heidelberg (2012)"},{"key":"14_CR14","unstructured":"ISO\/JTC1\/SC34. ISO\/IEC 19757-2:2008: Information Technology \u2013 Document Schema Definition Language (DSDL) \u2013 Part 2: Regular-grammar-based validation \u2013 RELAX NG. ISO\/IEC, http:\/\/relaxng.org"},{"key":"14_CR15","unstructured":"ISO\/JTC1\/SC34. ISO\/IEC 19757-3:2006: Information Technology - Document Schema Definition Languages (DSDL) - Part 3: Rule-based validation - Schematron. ISO\/IEC, http:\/\/schematron.com\/"},{"key":"14_CR16","unstructured":"ISO\/JTC1\/SC7\/WG19. ISO\/IEC 15909-2:2011. Systems and software engineering \u2013 High-level Petri nets \u2013 Part 2: Transfer format (2011)"},{"key":"14_CR17","unstructured":"Klai, K., Ochi, H.: Modular verification of inter-enterprise business processes. In: eKNOW, pp. 155\u2013161 (2012)"},{"key":"14_CR18","doi-asserted-by":"crossref","unstructured":"Kordon, F., Linard, A., Buchs, D., Colange, M., Evangelista, S., Fronc, L., Hillah, L.-M., Lohmann, N., Paviot-Adet, E., Pommereau, F., Rohr, C., Thierry-Mieg, Y., Wimmel, H., Wolf, K.: Raw report on the model checking contest at Petri nets, 2012. Technical report, CoRR (2012)","DOI":"10.1007\/978-3-642-35179-2_8"},{"key":"14_CR19","doi-asserted-by":"crossref","unstructured":"Lakos, C., Petrucci, L.: Modular analysis of systems composed of semiautonomous subsystems. In: ACSD, pp. 185\u2013196. IEEE Computer Society (2004)","DOI":"10.1109\/CSD.2004.1309131"},{"issue":"1-2","key":"14_CR20","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/s100090050010","volume":"1","author":"K.G. Larsen","year":"1997","unstructured":"Larsen, K.G., Pettersson, P., Yi, W.: UPPAAL in a nutshell. International Journal on Software Tools for Technology Transfer\u00a01(1-2), 134\u2013152 (1997)","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"14_CR21","doi-asserted-by":"crossref","unstructured":"Liu, Y., Sun, J., Dong, J.S.: PAT 3: An extensible architecture for building multi-domain model checkers. In: ISSRE, pp. 190\u2013199. IEEE (2011)","DOI":"10.1109\/ISSRE.2011.19"},{"key":"14_CR22","unstructured":"Steinberg, D., Budinsky, F., Paternostro, M., Merks, E.: EMF: Eclipse Modeling Framework, 2nd edn. Eclipse Series. Addison-Wesley Professional (2008)"},{"key":"14_CR23","unstructured":"The CosyVerif group. CosyVerif Web page, http:\/\/www.cosyverif.org"},{"key":"14_CR24","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"559","DOI":"10.1007\/978-3-642-31365-3_44","volume-title":"Automated Reasoning","author":"M. Urbas","year":"2012","unstructured":"Urbas, M., Jamnik, M.: Diabelli: A heterogeneous proof system. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS(LNAI), vol.\u00a07364, pp. 559\u2013566. Springer, Heidelberg (2012)"}],"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-41202-8_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T17:42:48Z","timestamp":1746034968000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-41202-8_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642412011","9783642412028"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-41202-8_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}