{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T04:01:43Z","timestamp":1775880103683,"version":"3.50.1"},"publisher-location":"Cham","reference-count":89,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030002435","type":"print"},{"value":"9783030002442","type":"electronic"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","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":[[2018]]},"DOI":"10.1007\/978-3-030-00244-2_13","type":"book-chapter","created":{"date-parts":[[2018,8,30]],"date-time":"2018-08-30T04:12:38Z","timestamp":1535602358000},"page":"189-210","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":17,"title":["Compositional Verification in Action"],"prefix":"10.1007","author":[{"given":"Hubert","family":"Garavel","sequence":"first","affiliation":[]},{"given":"Fr\u00e9d\u00e9ric","family":"Lang","sequence":"additional","affiliation":[]},{"given":"Laurent","family":"Mounier","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2018,8,30]]},"reference":[{"key":"13_CR1","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/BF00262973","volume":"17","author":"A Arnold","year":"1982","unstructured":"Arnold, A.: Synchronized behaviours of processes and rational relations. Acta Inf. 17, 21\u201329 (1982)","journal-title":"Acta Inf."},{"key":"13_CR2","doi-asserted-by":"crossref","unstructured":"Attali, I., Barros, T., Madelaine, E.: Parameterized specification and verification of the Chilean electronic invoices system. In: Proceedings of the 24th International Conference of the Chilean Computer Science Society (SCCC 2004), Arica, Chili, pp. 14\u201325. Society for Computer Simulation International, IEEE, November 2004","DOI":"10.1109\/QEST.2004.16"},{"key":"13_CR3","unstructured":"Bainbridge, S., Mounier, L.: Specification and verification of a reliable multicast protocol. Technical report HPL-91-163, Hewlett-Packard Laboratories, Bristol, UK, October 1991"},{"key":"13_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/11537328_14","volume-title":"Model Checking Software","author":"T Barros","year":"2005","unstructured":"Barros, T., Henrio, L., Madelaine, E.: Behavioural models for hierarchical components. In: Godefroid, P. (ed.) SPIN 2005. LNCS, vol. 3639, pp. 154\u2013168. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11537328_14"},{"key":"13_CR5","doi-asserted-by":"crossref","unstructured":"Barros, T., Henrio, L., Madelaine, E.: Verification of distributed hierarchical components. In: Proceedings of the International Workshop on Formal Aspects of Component Software (FACS 2005), Macao. Electronic Notes in Theoretical Computer Science, October 2005","DOI":"10.1016\/j.entcs.2006.05.014"},{"key":"13_CR6","unstructured":"Barros, T., Madelaine, E.: Formalization and proofs of the Chilean electronic invoices system. INRIA Research Report 5527, INRIA, June 2004"},{"key":"13_CR7","volume-title":"Handbook of Process Algebra","year":"2001","unstructured":"Bergstra, J.A., Ponse, A., Smolka, S.A. (eds.): Handbook of Process Algebra. Elsevier, Amsterdam (2001)"},{"key":"13_CR8","doi-asserted-by":"crossref","unstructured":"B\u00f6de, E., et al.: Compositional performability evaluation for Statemate. In: Proceedings of the 3rd International Conference on the Quantitative Evaluation of Systems (QUEST 2006), Riverside, California, USA, pp. 167\u2013178. IEEE Computer Society Press, September 2006","DOI":"10.1109\/QEST.2006.10"},{"issue":"3","key":"13_CR9","doi-asserted-by":"publisher","first-page":"381","DOI":"10.1007\/s00165-016-0366-2","volume":"28","author":"A Boulgakov","year":"2016","unstructured":"Boulgakov, A., Gibson-Robinson, T., Roscoe, A.W.: Computing maximal weak and other bisimulations. Form. Asp. Comput. 28(3), 381\u2013407 (2016)","journal-title":"Form. Asp. Comput."},{"key":"13_CR10","doi-asserted-by":"crossref","unstructured":"Bouzafour, A., Renaudin, M., Garavel, H., Mateescu, R., Serwe, W.: Model-checking synthesizable SystemVerilog descriptions of asynchronous circuits. In: Krstic, M., Jones, I.W. (eds.) Proceedings of the 24th IEEE International Symposium on Asynchronous Circuits and Systems (ASYNC 2018), Vienna, Austria. IEEE, May 2018","DOI":"10.1109\/ASYNC.2018.00021"},{"key":"13_CR11","doi-asserted-by":"crossref","unstructured":"Chehaibar, G., Garavel, H., Mounier, L., Tawbi, N., Zulian, F.: Specification and verification of the PowerScale bus arbitration protocol: an industrial experiment with LOTOS. In: Gotzhein, R., Bredereke, J. (eds.) Proceedings of the IFIP Joint International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols, and Protocol Specification, Testing, and Verification (FORTE\/PSTV 1996), Kaiserslautern, Germany, pp. 435\u2013450. Chapman & Hall, October 1996. Full version available as INRIA Research Report RR-2958","DOI":"10.1007\/978-0-387-35079-0_28"},{"key":"13_CR12","doi-asserted-by":"crossref","unstructured":"Cheung, S.C., Kramer, J.: Enhancing compositional reachability analysis with context constraints. In: Proceedings of the 1st ACM SIGSOFT International Symposium on the Foundations of Software Engineering, Los Angeles, CA, USA, pp. 115\u2013125. ACM Press, December 1993","DOI":"10.1145\/256428.167071"},{"key":"13_CR13","doi-asserted-by":"crossref","unstructured":"Cheung, S.C., Kramer, J.: Compositional reachability analysis of finite-state distributed systems with user-specified constraints. In: Proceedings of the 3rd ACM SIGSOFT International Symposium on the Foundations of Software Engineering, Washington, DC, USA, pp. 140\u2013150. ACM Press, October 1995","DOI":"10.1145\/222124.222149"},{"issue":"4","key":"13_CR14","doi-asserted-by":"publisher","first-page":"334","DOI":"10.1145\/235321.235323","volume":"5","author":"SC Cheung","year":"1996","unstructured":"Cheung, S.C., Kramer, J.: Context constraints for compositional reachability. ACM Trans. Softw. Eng. Methodol. (TOSEM) 5(4), 334\u2013377 (1996)","journal-title":"ACM Trans. Softw. Eng. Methodol. (TOSEM)"},{"key":"13_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/10722167_15","volume-title":"Computer Aided Verification","author":"E Clarke","year":"2000","unstructured":"Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 154\u2013169. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/10722167_15"},{"key":"13_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1007\/978-3-642-19811-3_9","volume-title":"Fundamental Approaches to Software Engineering","author":"P Crouzen","year":"2011","unstructured":"Crouzen, P., Lang, F.: Smart reduction. In: Giannakopoulou, D., Orejas, F. (eds.) FASE 2011. LNCS, vol. 6603, pp. 111\u2013126. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-19811-3_9"},{"key":"13_CR17","unstructured":"Fernandez, J.C.: ALDEBARAN: un syst\u00e8me de v\u00e9rification par r\u00e9duction de processus communicants. Th\u00e8se de Doctorat, Universit\u00e9 Joseph Fourier (Grenoble), May 1988"},{"key":"13_CR18","doi-asserted-by":"crossref","unstructured":"Fernandez, J.C., Garavel, H., Mounier, L., Rasse, A., Rodr\u00edguez, C., Sifakis, J.: A toolbox for the verification of LOTOS programs. In: Clarke, L.A. (ed.) Proceedings of the 14th International Conference on Software Engineering (ICSE \u201914), Melbourne, Australia, pp. 246\u2013259. ACM, May 1992","DOI":"10.1145\/143062.143124"},{"key":"13_CR19","doi-asserted-by":"crossref","unstructured":"Fogel, J.: A survey of verification techniques for solving the state explosion problem. In: Proceedings of the IFAC Conference on Control Systems Design (CSD 2000), Bratislava, Slovak Republic, IFAC Proceedings Volumes, vol. 33(13), pp. 361\u2013366, June 2000","DOI":"10.1016\/S1474-6670(17)37216-6"},{"key":"13_CR20","unstructured":"Furia, C.: A compositional world: a survey of recent works on compositionality in formal methods. Technical report 2005.22, Dipartimento di Elettronica e Informazione, Politecnico di Milano, Italy, March 2005"},{"key":"13_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1007\/BFb0054165","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"H Garavel","year":"1998","unstructured":"Garavel, H.: OPEN\/C\u00c6SAR: an open software architecture for verification, simulation, and testing. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol. 1384, pp. 68\u201384. Springer, Heidelberg (1998). https:\/\/doi.org\/10.1007\/BFb0054165 . Full version available as INRIA Research Report RR-3352"},{"key":"13_CR22","unstructured":"Garavel, H., Graf, S.: Formal methods for safe and secure computers systems. BSI Study 875, Bundesamt f\u00fcr Sicherheit in der Informationstechnik, Bonn, Germany, December 2013"},{"key":"13_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"410","DOI":"10.1007\/3-540-45614-7_23","volume-title":"FME 2002: Formal Methods\u2014Getting IT Right","author":"H Garavel","year":"2002","unstructured":"Garavel, H., Hermanns, H.: On combining functional verification and performance evaluation using CADP. In: Eriksson, L.-H., Lindsay, P.A. (eds.) FME 2002. LNCS, vol. 2391, pp. 410\u2013429. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45614-7_23 . Full version available as INRIA Research Report 4492"},{"key":"13_CR24","doi-asserted-by":"crossref","unstructured":"Garavel, H., Lang, F.: SVL: a scripting language for compositional verification. In: Kim, M., Chin, B., Kang, S., Lee, D. (eds.) Proceedings of the 21st IFIP WG 6.1 International Conference on Formal Techniques for Networked and Distributed Systems (FORTE 2001), Cheju Island, Korea, pp. 377\u2013392. Kluwer Academic Publishers, August 2001. Full version available as INRIA Research Report RR-4223","DOI":"10.1007\/0-306-47003-9_24"},{"issue":"4","key":"13_CR25","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/s00236-015-0226-1","volume":"52","author":"H Garavel","year":"2015","unstructured":"Garavel, H., Lang, F., Mateescu, R.: Compositional verification of asynchronous concurrent systems using CADP. Acta Inform. 52(4), 337\u2013392 (2015)","journal-title":"Acta Inform."},{"issue":"2","key":"13_CR26","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1007\/s10009-012-0244-z","volume":"15","author":"H Garavel","year":"2013","unstructured":"Garavel, H., Lang, F., Mateescu, R., Serwe, W.: CADP 2011: a toolbox for the construction and analysis of distributed processes. Springer Int. J. Softw. Tools Technol. Transf. (STTT) 15(2), 89\u2013107 (2013)","journal-title":"Springer Int. J. Softw. Tools Technol. Transf. (STTT)"},{"key":"13_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-319-68270-9_1","volume-title":"ModelEd, TestEd, TrustEd: Essays Dedicated to Ed Brinksma on the Occasion of His 60th Birthday","author":"H Garavel","year":"2017","unstructured":"Garavel, H., Lang, F., Serwe, W.: From LOTOS to LNT. In: Katoen, J.-P., Langerak, R., Rensink, A. (eds.) ModelEd, TestEd, TrustEd. LNCS, vol. 10500, pp. 3\u201326. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-68270-9_1"},{"issue":"1\u20132","key":"13_CR28","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1016\/S0167-6423(96)00034-2","volume":"29","author":"H Garavel","year":"1997","unstructured":"Garavel, H., Mounier, L.: Specification and verification of various distributed leader election algorithms for unidirectional ring networks. Sci. Comput. Program. 29(1\u20132), 171\u2013197 (1997). Special issue on Industrially Relevant Applications of Formal Analysis Techniques. Full version available as INRIA Research Report RR-2986","journal-title":"Sci. Comput. Program."},{"key":"13_CR29","doi-asserted-by":"crossref","unstructured":"Garavel, H., Sighireanu, M.: A graphical parallel composition operator for process algebras. In: Wu, J., Gao, Q., Chanson, S.T. (eds.) Proceedings of the IFIP Joint International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols, and Protocol Specification, Testing, and Verification (FORTE\/PSTV 1999), Beijing, China, pp. 185\u2013202. Kluwer Academic Publishers, October 1999","DOI":"10.1007\/978-0-387-35578-8_11"},{"key":"13_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1007\/978-3-642-02652-2_20","volume-title":"Model Checking Software","author":"H Garavel","year":"2009","unstructured":"Garavel, H., Thivolle, D.: Verification of GALS systems by combining synchronous languages and process calculi. In: P\u0103s\u0103reanu, C.S. (ed.) SPIN 2009. LNCS, vol. 5578, pp. 241\u2013260. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02652-2_20"},{"issue":"3","key":"13_CR31","doi-asserted-by":"crossref","first-page":"314","DOI":"10.1007\/s100090100044","volume":"3","author":"H Garavel","year":"2001","unstructured":"Garavel, H., Viho, C., Zendri, M.: System design of a CC-NUMA multiprocessor architecture using formal specification, model-checking, co-simulation, and test generation. Springer Int. J. Softw. Tools Technol. Transf. (STTT) 3(3), 314\u2013331 (2001). Also available as INRIA Research Report RR-4041","journal-title":"Springer Int. J. Softw. Tools Technol. Transf. (STTT)"},{"key":"13_CR32","unstructured":"Giannakopoulou, D.: Model checking for concurrent software architectures. Ph.D. thesis, Imperial College of Science, Technology and Medicine, University of London, Department of Computer Science, January 1999"},{"key":"13_CR33","doi-asserted-by":"publisher","first-page":"345","DOI":"10.1007\/978-3-319-10575-8_12","volume-title":"Handbook of Model Checking","author":"D Giannakopoulou","year":"2018","unstructured":"Giannakopoulou, D., Namjoshi, K.S., P\u0103s\u0103reanu, C.S.: Compositional reasoning. In: Clarke, E., Henzinger, T., Veith, H., Bloem, R. (eds.) Handbook of Model Checking, pp. 345\u2013383. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8_12"},{"issue":"3","key":"13_CR34","doi-asserted-by":"publisher","first-page":"555","DOI":"10.1145\/233551.233556","volume":"43","author":"RJ Glabbeek van","year":"1996","unstructured":"van Glabbeek, R.J., Weijland, W.P.: Branching time and abstraction in bisimulation semantics. J. ACM 43(3), 555\u2013600 (1996)","journal-title":"J. ACM"},{"key":"13_CR35","unstructured":"Godza, G., Cristea, V., Mateescu, R.: Formal specification of checkpointing algorithms. In: Proceedings of 13th International Conference on Control Systems and Computer Science (CSCS 2013), Bucharest, Romania, pp. 311\u2013317. Polytechnic University of Bucharest, May 2001"},{"key":"13_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"186","DOI":"10.1007\/BFb0023732","volume-title":"Computer-Aided Verification","author":"S Graf","year":"1991","unstructured":"Graf, S., Steffen, B.: Compositional minimization of finite state systems. In: Clarke, E.M., Kurshan, R.P. (eds.) CAV 1990. LNCS, vol. 531, pp. 186\u2013196. Springer, Heidelberg (1991). https:\/\/doi.org\/10.1007\/BFb0023732"},{"key":"13_CR37","doi-asserted-by":"crossref","unstructured":"Graf, S., Steffen, B.: Compositional minimization of finite state systems. Aachener Informatik-Berichte AIB 1991-23, RWTH Aachen University, Department of Computer Science, Germany (1991)","DOI":"10.1090\/dimacs\/003\/06"},{"key":"13_CR38","unstructured":"Graf, S., Steffen, B., L\u00fcttgen, G.: Compositional minimization of finite state systems using interface specifications. Research Report MIP-9505, Universit\u00e4t Passau, Fakult\u00e4t f\u00fcr Mathematik und Informatik, Germany (1995)"},{"issue":"5","key":"13_CR39","doi-asserted-by":"publisher","first-page":"607","DOI":"10.1007\/BF01211911","volume":"8","author":"S Graf","year":"1996","unstructured":"Graf, S., Steffen, B., L\u00fcttgen, G.: Compositional minimization of finite state systems using interface specifications. Form. Asp. Comput. 8(5), 607\u2013616 (1996). 10-page article published in the paper version of the journal","journal-title":"Form. Asp. Comput."},{"key":"13_CR40","unstructured":"Graf, S., Steffen, B., L\u00fcttgen, G.: Compositional minimization of finite state systems using interface specifications. Form. Asp. Comput. 8E, 286\u2013313 (1996). 28-page article published in the electronic repository of the journal. http:\/\/static-content.springer.com\/esm\/art%3A10.1007%2FBF01211911\/MediaObjects\/165_2005_BF01211911_MOESM1_ESM.pdf"},{"key":"13_CR41","doi-asserted-by":"crossref","unstructured":"He, J., Turner, K.J.: Specification and verification of synchronous hardware using LOTOS. In: Wu, J., Chanson, S.T., Gao, Q. (eds.) Proceedings of the IFIP Joint International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols and Protocol Specification, Testing, and Verification (FORTE\/PSTV 1999), Beijing, China, pp. 295\u2013312. Kluwer Academic Publishers, October 1999","DOI":"10.1007\/978-0-387-35578-8_17"},{"key":"13_CR42","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45804-2","volume-title":"Interactive Markov Chains: And the Quest for Quantified Quality","author":"H Hermanns","year":"2002","unstructured":"Hermanns, H.: Interactive Markov Chains. LNCS, vol. 2428. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45804-2"},{"key":"13_CR43","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1016\/S0167-6423(99)00019-2","volume":"36","author":"H Hermanns","year":"2000","unstructured":"Hermanns, H., Katoen, J.P.: Automated compositional Markov chain generation for a plain-old telephone system. Sci. Comput. Program. 36, 97\u2013127 (2000)","journal-title":"Sci. Comput. Program."},{"issue":"8","key":"13_CR44","doi-asserted-by":"publisher","first-page":"666","DOI":"10.1145\/359576.359585","volume":"21","author":"CAR Hoare","year":"1978","unstructured":"Hoare, C.A.R.: Communicating sequential processes. Commun. ACM 21(8), 666\u2013677 (1978)","journal-title":"Commun. ACM"},{"key":"13_CR45","volume-title":"Communicating Sequential Processes","author":"CAR Hoare","year":"1985","unstructured":"Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Englewood Cliffs (1985)"},{"key":"13_CR46","unstructured":"ISO\/IEC: LOTOS - A Formal Description Technique Based on the Temporal Ordering of Observational Behaviour. International Standard 8807, International Organization for Standardization - Information Processing Systems - Open Systems Interconnection, Geneva, September 1989"},{"key":"13_CR47","unstructured":"de Jacquier, A., Massart, T., Hernalsteen, C.: V\u00e9rification et correction d\u2019un protocole de contr\u00f4le a\u00e9rien. Technical report 363, Universit\u00e9 Libre de Bruxelles, May 1997"},{"key":"13_CR48","series-title":"IFIP Advances in Information and Communication Technology","doi-asserted-by":"publisher","first-page":"303","DOI":"10.1007\/978-0-387-34945-9_22","volume-title":"Formal Description Techniques VIII","author":"A Kerbrat","year":"1996","unstructured":"Kerbrat, A., Ben Atallah, S.: Formal specification of a framework for groupware development. In: Bochmann, G., Dssouli, R., Rafiq, O. (eds.) FORTE 1995. IFIPAICT, pp. 303\u2013310. Springer, Boston (1996). https:\/\/doi.org\/10.1007\/978-0-387-34945-9_22"},{"key":"13_CR49","doi-asserted-by":"crossref","unstructured":"Kordon, F., et al.: MCC\u20192017 - The Seventh Model Checking Contest. Transactions on Petri Nets and Other Models of Concurrency (2018, to appear)","DOI":"10.1007\/978-3-662-58381-4_9"},{"key":"13_CR50","unstructured":"Krimm, J.-P.: Une approche compositionnelle pour la v\u00e9rification de programmes LOTOS. Master\u2019s thesis, Universit\u00e9 Joseph Fourier (Grenoble), June 1996"},{"key":"13_CR51","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1007\/BFb0035392","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J-P Krimm","year":"1997","unstructured":"Krimm, J.-P., Mounier, L.: Compositional state space generation from LOTOS programs. In: Brinksma, E. (ed.) TACAS 1997. LNCS, vol. 1217, pp. 239\u2013258. Springer, Heidelberg (1997). https:\/\/doi.org\/10.1007\/BFb0035392 . Extended version with proofs available as Research Report VERIMAG RR97-01"},{"key":"13_CR52","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"465","DOI":"10.1007\/3-540-46002-0_33","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"F Lang","year":"2002","unstructured":"Lang, F.: Compositional verification using SVL scripts. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, pp. 465\u2013469. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-46002-0_33"},{"key":"13_CR53","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"159","DOI":"10.1007\/11888116_13","volume-title":"Formal Techniques for Networked and Distributed Systems - FORTE 2006","author":"F Lang","year":"2006","unstructured":"Lang, F.: Refined interfaces for compositional verification. In: Najm, E., Pradat-Peyre, J.-F., Vigui\u00e9 Donzeau-Gouge, V. (eds.) FORTE 2006. LNCS, vol. 4229, pp. 159\u2013174. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11888116_13 . Full version available as INRIA Research Report RR-5996"},{"key":"13_CR54","unstructured":"Luukkainen, M., Ahtiainen, A.: Compositional verification of large SDL systems. In: Proceedings of the 1st Workshop of the SDL Forum Society on SDL and MSC (SAM 1998), Berlin, Germany, June 1998"},{"key":"13_CR55","doi-asserted-by":"crossref","unstructured":"Malhotra, J., Smolka, S.A., Giacalone, A., Shapiro, R.: A tool for hierarchical design and simulation of concurrent systems. In: Proceedings of the BCS-FACS Workshop on Specification and Verification of Concurrent Systems, Stirling, Scotland, UK, pp. 140\u2013152. British Computer Society, July 1988","DOI":"10.1007\/978-1-4471-3534-0_7"},{"key":"13_CR56","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"180","DOI":"10.1007\/978-3-642-15898-8_12","volume-title":"Formal Methods for Industrial Critical Systems","author":"R Mateescu","year":"2010","unstructured":"Mateescu, R., Serwe, W.: A study of shared-memory mutual exclusion protocols using CADP. In: Kowalewski, S., Roveri, M. (eds.) FMICS 2010. LNCS, vol. 6371, pp. 180\u2013197. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-15898-8_12"},{"issue":"7","key":"13_CR57","doi-asserted-by":"publisher","first-page":"843","DOI":"10.1016\/j.scico.2012.01.003","volume":"78","author":"R Mateescu","year":"2013","unstructured":"Mateescu, R., Serwe, W.: Model checking and performance evaluation with CADP illustrated on shared-memory mutual exclusion protocols. Sci. Comput. Program. 78(7), 843\u2013861 (2013)","journal-title":"Sci. Comput. Program."},{"key":"13_CR58","doi-asserted-by":"crossref","unstructured":"Mazzanti, F., Ferrari, A.: Ten diverse formal models for a CBTC automatic train supervision system. In: Gallagher, J.P., van Glabbeek, R., Serwe, W. (eds.) Proceedings of the 3rd Workshop on Models for Formal Analysis of Real Systems and the 6th International Workshop on Verification and Program Transformation (MARS\/VPT 2018), Thessaloniki, Greece. Electronic Proceedings in Theoretical Computer Science, vol. 268, pp. 104\u2013149, April 2018","DOI":"10.4204\/EPTCS.268.4"},{"issue":"3","key":"13_CR59","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/s10009-018-0488-3","volume":"20","author":"F Mazzanti","year":"2018","unstructured":"Mazzanti, F., Ferrari, A., Spagnolo, G.O.: Towards formal methods diversity in railways: an experience report with seven frameworks. Springer Int. J. Softw. Tools Technol. Transf. (STTT) 20(3), 263\u2013288 (2018)","journal-title":"Springer Int. J. Softw. Tools Technol. Transf. (STTT)"},{"issue":"6","key":"13_CR60","doi-asserted-by":"publisher","first-page":"749","DOI":"10.1093\/bioinformatics\/btt033","volume":"29","author":"N Mendes","year":"2013","unstructured":"Mendes, N., Lang, F., Cornec, Y.S.L., Mateescu, R., Batt, G., Chaouiya, C.: Composition and abstraction of logical regulatory modules: application to multicellular systems. Bioinformatics 29(6), 749\u2013757 (2013)","journal-title":"Bioinformatics"},{"key":"13_CR61","doi-asserted-by":"publisher","unstructured":"Milner, R. : A Calculus of Communicating Systems. LNCS, vol. 92. Springer, Heidelberg (1980). https:\/\/doi.org\/10.1007\/3-540-10235-3","DOI":"10.1007\/3-540-10235-3"},{"key":"13_CR62","unstructured":"Mounier, L.: A LOTOS specification of a transit-node. Rapport SPECTRE 94-8, VERIMAG, Grenoble, March 1994"},{"key":"13_CR63","doi-asserted-by":"crossref","unstructured":"Oliveira, R., Dupuy-Chessa, S., Calvary, G., Dadolle, D.: Using formal models to cross check an implementation. In: Luyten, K., Palanque, P. (eds.) Proceedings of the 8th ACM SIGCHI Symposium on Engineering Interactive Computing Systems (EICS 2016), Brussels, Belgium, pp. 126\u2013137. ACM, June 2016","DOI":"10.1145\/2933242.2933257"},{"key":"13_CR64","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/BFb0017309","volume-title":"Theoretical Computer Science","author":"D Park","year":"1981","unstructured":"Park, D.: Concurrency and automata on infinite sequences. In: Deussen, P. (ed.) GI-TCS 1981. LNCS, vol. 104, pp. 167\u2013183. Springer, Heidelberg (1981). https:\/\/doi.org\/10.1007\/BFb0017309"},{"key":"13_CR65","doi-asserted-by":"crossref","unstructured":"Pecheur, C.: Advanced modelling and verification techniques applied to a cluster file system. In: Hall, R.J., Tyugu, E. (eds.) Proceedings of the 14th IEEE International Conference on Automated Software Engineering (ASE 1999), Cocoa Beach, Florida, USA. IEEE Computer Society, October 1999. Extended version available as INRIA Research Report RR-3416","DOI":"10.1109\/ASE.1999.802152"},{"key":"13_CR66","unstructured":"Peng, H., Tahar, S.: A survey on compositional verification. Technical report, Department of Electrical and Computer Engineering, Concordia University, Montreal, Canada, November 1998"},{"key":"13_CR67","series-title":"Cambridge Tracts in Theoretical Computer Science","volume-title":"Concurrency Verification - Introduction to Compositional and Noncompositional Methods","author":"W Roever","year":"2001","unstructured":"Roever, W., et al.: Concurrency Verification - Introduction to Compositional and Noncompositional Methods. Cambridge Tracts in Theoretical Computer Science, vol. 54. Cambridge University Press, Cambridge (2001)"},{"key":"13_CR68","unstructured":"Romijn, J.: Analysing industrial protocols with formal methods. Ph.D. thesis, University of Twente, The Netherlands, September 1999"},{"issue":"9","key":"13_CR69","doi-asserted-by":"publisher","first-page":"940","DOI":"10.1109\/26.35374","volume":"37","author":"KK Sabnani","year":"1989","unstructured":"Sabnani, K.K., Lapone, A.M., Uyar, M.U.: An algorithmic procedure for checking safety properties of protocols. IEEE Trans. Commun. 37(9), 940\u2013948 (1989)","journal-title":"IEEE Trans. Commun."},{"key":"13_CR70","unstructured":"Sage, M., Johnson, C.: A declarative prototyping environment for the development of multi-user safety-critical systems. In: Proceedings of the 17th International System Safety Conference (ISSC 1999) Orlando, Florida, USA. System Safety Society, August 1999"},{"key":"13_CR71","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/978-3-642-00255-7_12","volume-title":"Integrated Formal Methods","author":"G Sala\u00fcn","year":"2009","unstructured":"Sala\u00fcn, G., Bultan, T.: Realizability of choreographies using process algebra encodings. In: Leuschel, M., Wehrheim, H. (eds.) IFM 2009. LNCS, vol. 5423, pp. 167\u2013182. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-00255-7_12"},{"key":"13_CR72","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1007\/11589976_17","volume-title":"Integrated Formal Methods","author":"G Sala\u00fcn","year":"2005","unstructured":"Sala\u00fcn, G., Serwe, W.: Translating hardware process algebras into standard process algebras: illustration with CHP and LOTOS. In: Romijn, J., Smith, G., van de Pol, J. (eds.) IFM 2005. LNCS, vol. 3771, pp. 287\u2013306. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11589976_17 . Full version available as INRIA Research Report RR-5666"},{"key":"13_CR73","doi-asserted-by":"crossref","unstructured":"Sala\u00fcn, G., Serwe, W., Thonnart, Y., Vivet, P.: Formal verification of CHP specifications with CADP - illustration on an asynchronous network-on-chip. In: Beerel, P., Roncken, M., Greenstreet, M., Singh, M. (eds.) Proceedings of the 13th IEEE International Symposium on Asynchronous Circuits and Systems (ASYNC 2007), Berkeley, California, USA, pp. 73\u201382. IEEE Computer Society Press, March 2007","DOI":"10.1109\/ASYNC.2007.18"},{"key":"13_CR74","unstructured":"Schieferdecker, I.: Abruptly-terminated connections in TCP - a verification example. In: Brezo\u010dnik, Z., Kapus, T. (eds.) Proceedings of the COST 247 International Workshop on Applied Formal Methods in System Design, Maribor, Slovenia, pp. 136\u2013145. University of Maribor, Slovenia, June 1996"},{"key":"13_CR75","doi-asserted-by":"crossref","unstructured":"Serwe, W.: Formal specification and verification of fully asynchronous implementations of the data encryption standard. In: van Glabbeek, R., Groote, J.F., H\u00f6fner, P. (eds.) Proceedings of the International Workshop on Models for Formal Analysis of Real Systems (MARS 2015), Suva, Fiji. Electronic Proceedings in Theoretical Computer Science, vol. 196 (2015)","DOI":"10.4204\/EPTCS.196.6"},{"key":"13_CR76","unstructured":"Tai, K.C., Koppol, V.: An incremental approach to reachability analysis of distributed programs. In: Proceedings of the 7th International Workshop on Software Specification and Design, Los Angeles, CA, USA, pp. 141\u2013150. IEEE Press, Piscataway, December 1993"},{"key":"13_CR77","doi-asserted-by":"crossref","unstructured":"Tai, K.C., Koppol, V.: Hierarchy-based incremental reachability analysis of communication protocols. In: Proceedings of the IEEE International Conference on Network Protocols, San Francisco, CA, USA, pp. 318\u2013325. IEEE Press, Piscataway, October 1993","DOI":"10.1109\/ICNP.1993.340896"},{"key":"13_CR78","unstructured":"Tan, L.: Case studies using CRESS to develop web and grid services. Technical report, Department of Computing Science and Mathematics, University of Stirling, Scotland, UK, December 2009"},{"key":"13_CR79","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1007\/978-3-540-39958-2_17","volume-title":"Formal Methods for Open Object-Based Distributed Systems","author":"F Tronel","year":"2003","unstructured":"Tronel, F., Lang, F., Garavel, H.: Compositional verification using CADP of the ScalAgent deployment protocol for software components. In: Najm, E., Nestmann, U., Stevens, P. (eds.) FMOODS 2003. LNCS, vol. 2884, pp. 244\u2013260. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/978-3-540-39958-2_17 . Full version available as INRIA Research Report RR-5012"},{"key":"13_CR80","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"427","DOI":"10.1007\/3-540-56689-9_54","volume-title":"Advances in Petri Nets 1993","author":"A Valmari","year":"1993","unstructured":"Valmari, A.: Compositional state space generation. In: Rozenberg, G. (ed.) ICATPN 1991. LNCS, vol. 674, pp. 427\u2013457. Springer, Heidelberg (1993). https:\/\/doi.org\/10.1007\/3-540-56689-9_54"},{"key":"13_CR81","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1007\/3-540-61363-3_3","volume-title":"Application and Theory of Petri Nets 1996","author":"A Valmari","year":"1996","unstructured":"Valmari, A.: Compositionality in state space verification methods. In: Billington, J., Reisig, W. (eds.) ICATPN 1996. LNCS, vol. 1091, pp. 29\u201356. Springer, Heidelberg (1996). https:\/\/doi.org\/10.1007\/3-540-61363-3_3"},{"key":"13_CR82","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"58","DOI":"10.1007\/3-540-45510-8_3","volume-title":"Modeling and Verification of Parallel Processes","author":"A Valmari","year":"2001","unstructured":"Valmari, A.: Composition and abstraction. In: Cassez, F., Jard, C., Rozoy, B., Ryan, M.D. (eds.) MOVEP 2000. LNCS, vol. 2067, pp. 58\u201398. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-45510-8_3"},{"key":"13_CR83","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"597","DOI":"10.1007\/BFb0024669","volume-title":"FME 1993: Industrial-Strength Formal Methods","author":"A Valmari","year":"1993","unstructured":"Valmari, A., Kemppainen, J., Clegg, M., Levanto, M.: Putting advanced reachability analysis techniques together: The \u201cARA\u201d tool. In: Woodcock, J.C.P., Larsen, P.G. (eds.) FME 1993. LNCS, vol. 670, pp. 597\u2013616. Springer, Heidelberg (1993). https:\/\/doi.org\/10.1007\/BFb0024669"},{"key":"13_CR84","doi-asserted-by":"crossref","unstructured":"Valmari, A., Kokkarinen, I.: Unbounded verification results by finite-state compositional techniques: $$10^{\\text{any}}$$ states and beyond. In: Proceedings of the 1st International Conference on Application of Concurrency to System Design (ACSD 1998), Fukushima, Japan, pp. 75\u201385. IEEE Computer Society, March 1998","DOI":"10.1109\/CSD.1998.657541"},{"key":"13_CR85","unstructured":"Willemse, T.: The specification and validation of the OM\/RR-protocol. Master\u2019s thesis, Department of Mathematics and Computing Science, Eindhoven University of Technology, Eindhoven, The Netherlands, June 1998"},{"key":"13_CR86","unstructured":"Willemse, T., Tretmans, J., Klomp, A.: A case study in formal methods: specification and validation of the OM\/RR protocol. In: Gnesi, S., Schieferdecker, I., Rennoch, A. (eds.) Proceedings of the 5th International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2000), Berlin, Germany, pp. 331\u2013344. GMD Report 91, Berlin, April 2000"},{"key":"13_CR87","unstructured":"Yeh, W.J.: Controlling state explosion in reachability analysis. Ph.D. thesis, Software Engineering Research Center (SERC) Laboratory, Purdue University, December 1993. Technical report SERC-TR-147-P"},{"key":"13_CR88","doi-asserted-by":"crossref","unstructured":"Yeh, W.J., Young, M.: Compositional reachability analysis using process algebra. In: Proceedings of the ACM SIGSOFT Symposium on Testing, Analysis, and Verification (SIGSOFT 1991), Victoria, British Columbia, Canada, pp. 49\u201359. ACM Press, October 1991","DOI":"10.1145\/120807.120812"},{"key":"13_CR89","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1016\/j.scico.2016.01.002","volume":"118","author":"Z Zhang","year":"2016","unstructured":"Zhang, Z., Serwe, W., Wu, J., Zheng, T.Y.H., Myers, C.: An improved fault-tolerant routing algorithm for a network-on-chip derived with formal analysis. Sci. Comput. Program. 118, 24\u201339 (2016)","journal-title":"Sci. Comput. Program."}],"container-title":["Lecture Notes in Computer Science","Formal Methods for Industrial Critical Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-00244-2_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,6]],"date-time":"2025-07-06T17:44:43Z","timestamp":1751823883000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-00244-2_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783030002435","9783030002442"],"references-count":89,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-00244-2_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018]]}}}