Advertisement

Compositional Verification in Action

  • Hubert Garavel
  • Frédéric Lang
  • Laurent Mounier
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11119)

Abstract

Concurrent systems are intrinsically complex and their verification is hampered by the well-known “state-space explosion” issue. Compositional verification is a powerful approach, based on the divide-and-conquer paradigm, to address this issue. Despite impressive results, this approach is not used widely enough in practice, probably because it exists under multiple variants that make knowledge of the field hard to attain. In this article, we highlight the seminal results of Graf & Steffen and propose a survey of compositional verification techniques that exploit (or not) these results.

Notes

Acknowledgements

The present work has been partly funded by Bpi France and Feder (Fonds Européen de Développement Economique Régional) Rhône-Alpes Auvergne under national project SecurIoT-2 supported by the four competitiveness clusters Minalogic, Scs, Systematic Paris-Région, and Derbi.

References

  1. 1.
    Arnold, A.: Synchronized behaviours of processes and rational relations. Acta Inf. 17, 21–29 (1982)MathSciNetCrossRefGoogle Scholar
  2. 2.
    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–25. Society for Computer Simulation International, IEEE, November 2004Google Scholar
  3. 3.
    Bainbridge, S., Mounier, L.: Specification and verification of a reliable multicast protocol. Technical report HPL-91-163, Hewlett-Packard Laboratories, Bristol, UK, October 1991Google Scholar
  4. 4.
    Barros, T., Henrio, L., Madelaine, E.: Behavioural models for hierarchical components. In: Godefroid, P. (ed.) SPIN 2005. LNCS, vol. 3639, pp. 154–168. Springer, Heidelberg (2005).  https://doi.org/10.1007/11537328_14CrossRefGoogle Scholar
  5. 5.
    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 2005Google Scholar
  6. 6.
    Barros, T., Madelaine, E.: Formalization and proofs of the Chilean electronic invoices system. INRIA Research Report 5527, INRIA, June 2004Google Scholar
  7. 7.
    Bergstra, J.A., Ponse, A., Smolka, S.A. (eds.): Handbook of Process Algebra. Elsevier, Amsterdam (2001)zbMATHGoogle Scholar
  8. 8.
    Böde, 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–178. IEEE Computer Society Press, September 2006Google Scholar
  9. 9.
    Boulgakov, A., Gibson-Robinson, T., Roscoe, A.W.: Computing maximal weak and other bisimulations. Form. Asp. Comput. 28(3), 381–407 (2016)MathSciNetCrossRefGoogle Scholar
  10. 10.
    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 2018Google Scholar
  11. 11.
    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–450. Chapman & Hall, October 1996. Full version available as INRIA Research Report RR-2958Google Scholar
  12. 12.
    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–125. ACM Press, December 1993Google Scholar
  13. 13.
    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–150. ACM Press, October 1995Google Scholar
  14. 14.
    Cheung, S.C., Kramer, J.: Context constraints for compositional reachability. ACM Trans. Softw. Eng. Methodol. (TOSEM) 5(4), 334–377 (1996)CrossRefGoogle Scholar
  15. 15.
    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–169. Springer, Heidelberg (2000).  https://doi.org/10.1007/10722167_15CrossRefGoogle Scholar
  16. 16.
    Crouzen, P., Lang, F.: Smart reduction. In: Giannakopoulou, D., Orejas, F. (eds.) FASE 2011. LNCS, vol. 6603, pp. 111–126. Springer, Heidelberg (2011).  https://doi.org/10.1007/978-3-642-19811-3_9CrossRefGoogle Scholar
  17. 17.
    Fernandez, J.C.: ALDEBARAN: un système de vérification par réduction de processus communicants. Thèse de Doctorat, Université Joseph Fourier (Grenoble), May 1988Google Scholar
  18. 18.
    Fernandez, J.C., Garavel, H., Mounier, L., Rasse, A., Rodríguez, 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 ’14), Melbourne, Australia, pp. 246–259. ACM, May 1992Google Scholar
  19. 19.
    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–366, June 2000Google Scholar
  20. 20.
    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 2005Google Scholar
  21. 21.
    Garavel, H.: OPEN/CÆSAR: an open software architecture for verification, simulation, and testing. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol. 1384, pp. 68–84. Springer, Heidelberg (1998).  https://doi.org/10.1007/BFb0054165. Full version available as INRIA Research Report RR-3352CrossRefGoogle Scholar
  22. 22.
    Garavel, H., Graf, S.: Formal methods for safe and secure computers systems. BSI Study 875, Bundesamt für Sicherheit in der Informationstechnik, Bonn, Germany, December 2013Google Scholar
  23. 23.
    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–429. Springer, Heidelberg (2002).  https://doi.org/10.1007/3-540-45614-7_23. Full version available as INRIA Research Report 4492CrossRefGoogle Scholar
  24. 24.
    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–392. Kluwer Academic Publishers, August 2001. Full version available as INRIA Research Report RR-4223Google Scholar
  25. 25.
    Garavel, H., Lang, F., Mateescu, R.: Compositional verification of asynchronous concurrent systems using CADP. Acta Inform. 52(4), 337–392 (2015)MathSciNetCrossRefGoogle Scholar
  26. 26.
    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–107 (2013)CrossRefGoogle Scholar
  27. 27.
    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–26. Springer, Cham (2017).  https://doi.org/10.1007/978-3-319-68270-9_1CrossRefGoogle Scholar
  28. 28.
    Garavel, H., Mounier, L.: Specification and verification of various distributed leader election algorithms for unidirectional ring networks. Sci. Comput. Program. 29(1–2), 171–197 (1997). Special issue on Industrially Relevant Applications of Formal Analysis Techniques. Full version available as INRIA Research Report RR-2986CrossRefGoogle Scholar
  29. 29.
    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–202. Kluwer Academic Publishers, October 1999Google Scholar
  30. 30.
    Garavel, H., Thivolle, D.: Verification of GALS systems by combining synchronous languages and process calculi. In: Păsăreanu, C.S. (ed.) SPIN 2009. LNCS, vol. 5578, pp. 241–260. Springer, Heidelberg (2009).  https://doi.org/10.1007/978-3-642-02652-2_20CrossRefGoogle Scholar
  31. 31.
    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–331 (2001). Also available as INRIA Research Report RR-4041zbMATHGoogle Scholar
  32. 32.
    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 1999Google Scholar
  33. 33.
    Giannakopoulou, D., Namjoshi, K.S., Păsăreanu, C.S.: Compositional reasoning. In: Clarke, E., Henzinger, T., Veith, H., Bloem, R. (eds.) Handbook of Model Checking, pp. 345–383. Springer, Cham (2018).  https://doi.org/10.1007/978-3-319-10575-8_12CrossRefGoogle Scholar
  34. 34.
    van Glabbeek, R.J., Weijland, W.P.: Branching time and abstraction in bisimulation semantics. J. ACM 43(3), 555–600 (1996)MathSciNetCrossRefGoogle Scholar
  35. 35.
    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–317. Polytechnic University of Bucharest, May 2001Google Scholar
  36. 36.
    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–196. Springer, Heidelberg (1991).  https://doi.org/10.1007/BFb0023732CrossRefGoogle Scholar
  37. 37.
    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)Google Scholar
  38. 38.
    Graf, S., Steffen, B., Lüttgen, G.: Compositional minimization of finite state systems using interface specifications. Research Report MIP-9505, Universität Passau, Fakultät für Mathematik und Informatik, Germany (1995)Google Scholar
  39. 39.
    Graf, S., Steffen, B., Lüttgen, G.: Compositional minimization of finite state systems using interface specifications. Form. Asp. Comput. 8(5), 607–616 (1996). 10-page article published in the paper version of the journalCrossRefGoogle Scholar
  40. 40.
    Graf, S., Steffen, B., Lüttgen, G.: Compositional minimization of finite state systems using interface specifications. Form. Asp. Comput. 8E, 286–313 (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
  41. 41.
    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–312. Kluwer Academic Publishers, October 1999Google Scholar
  42. 42.
    Hermanns, H.: Interactive Markov Chains. LNCS, vol. 2428. Springer, Heidelberg (2002).  https://doi.org/10.1007/3-540-45804-2CrossRefzbMATHGoogle Scholar
  43. 43.
    Hermanns, H., Katoen, J.P.: Automated compositional Markov chain generation for a plain-old telephone system. Sci. Comput. Program. 36, 97–127 (2000)CrossRefGoogle Scholar
  44. 44.
    Hoare, C.A.R.: Communicating sequential processes. Commun. ACM 21(8), 666–677 (1978)CrossRefGoogle Scholar
  45. 45.
    Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Englewood Cliffs (1985)zbMATHGoogle Scholar
  46. 46.
    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 1989Google Scholar
  47. 47.
    de Jacquier, A., Massart, T., Hernalsteen, C.: Vérification et correction d’un protocole de contrôle aérien. Technical report 363, Université Libre de Bruxelles, May 1997Google Scholar
  48. 48.
    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–310. Springer, Boston (1996).  https://doi.org/10.1007/978-0-387-34945-9_22CrossRefGoogle Scholar
  49. 49.
    Kordon, F., et al.: MCC’2017 - The Seventh Model Checking Contest. Transactions on Petri Nets and Other Models of Concurrency (2018, to appear)Google Scholar
  50. 50.
    Krimm, J.-P.: Une approche compositionnelle pour la vérification de programmes LOTOS. Master’s thesis, Université Joseph Fourier (Grenoble), June 1996Google Scholar
  51. 51.
    Krimm, J.-P., Mounier, L.: Compositional state space generation from LOTOS programs. In: Brinksma, E. (ed.) TACAS 1997. LNCS, vol. 1217, pp. 239–258. Springer, Heidelberg (1997).  https://doi.org/10.1007/BFb0035392. Extended version with proofs available as Research Report VERIMAG RR97-01CrossRefGoogle Scholar
  52. 52.
    Lang, F.: Compositional verification using SVL scripts. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, pp. 465–469. Springer, Heidelberg (2002).  https://doi.org/10.1007/3-540-46002-0_33CrossRefGoogle Scholar
  53. 53.
    Lang, F.: Refined interfaces for compositional verification. In: Najm, E., Pradat-Peyre, J.-F., Viguié Donzeau-Gouge, V. (eds.) FORTE 2006. LNCS, vol. 4229, pp. 159–174. Springer, Heidelberg (2006).  https://doi.org/10.1007/11888116_13. Full version available as INRIA Research Report RR-5996CrossRefGoogle Scholar
  54. 54.
    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 1998Google Scholar
  55. 55.
    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–152. British Computer Society, July 1988Google Scholar
  56. 56.
    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–197. Springer, Heidelberg (2010).  https://doi.org/10.1007/978-3-642-15898-8_12CrossRefGoogle Scholar
  57. 57.
    Mateescu, R., Serwe, W.: Model checking and performance evaluation with CADP illustrated on shared-memory mutual exclusion protocols. Sci. Comput. Program. 78(7), 843–861 (2013)CrossRefGoogle Scholar
  58. 58.
    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–149, April 2018Google Scholar
  59. 59.
    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–288 (2018)CrossRefGoogle Scholar
  60. 60.
    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–757 (2013)CrossRefGoogle Scholar
  61. 61.
    Milner, R. : A Calculus of Communicating Systems. LNCS, vol. 92. Springer, Heidelberg (1980).  https://doi.org/10.1007/3-540-10235-3
  62. 62.
    Mounier, L.: A LOTOS specification of a transit-node. Rapport SPECTRE 94-8, VERIMAG, Grenoble, March 1994Google Scholar
  63. 63.
    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–137. ACM, June 2016Google Scholar
  64. 64.
    Park, D.: Concurrency and automata on infinite sequences. In: Deussen, P. (ed.) GI-TCS 1981. LNCS, vol. 104, pp. 167–183. Springer, Heidelberg (1981).  https://doi.org/10.1007/BFb0017309CrossRefGoogle Scholar
  65. 65.
    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-3416Google Scholar
  66. 66.
    Peng, H., Tahar, S.: A survey on compositional verification. Technical report, Department of Electrical and Computer Engineering, Concordia University, Montreal, Canada, November 1998Google Scholar
  67. 67.
    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)zbMATHGoogle Scholar
  68. 68.
    Romijn, J.: Analysing industrial protocols with formal methods. Ph.D. thesis, University of Twente, The Netherlands, September 1999Google Scholar
  69. 69.
    Sabnani, K.K., Lapone, A.M., Uyar, M.U.: An algorithmic procedure for checking safety properties of protocols. IEEE Trans. Commun. 37(9), 940–948 (1989)CrossRefGoogle Scholar
  70. 70.
    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 1999Google Scholar
  71. 71.
    Salaün, G., Bultan, T.: Realizability of choreographies using process algebra encodings. In: Leuschel, M., Wehrheim, H. (eds.) IFM 2009. LNCS, vol. 5423, pp. 167–182. Springer, Heidelberg (2009).  https://doi.org/10.1007/978-3-642-00255-7_12CrossRefGoogle Scholar
  72. 72.
    Salaün, 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–306. Springer, Heidelberg (2005).  https://doi.org/10.1007/11589976_17. Full version available as INRIA Research Report RR-5666CrossRefGoogle Scholar
  73. 73.
    Salaün, 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–82. IEEE Computer Society Press, March 2007Google Scholar
  74. 74.
    Schieferdecker, I.: Abruptly-terminated connections in TCP - a verification example. In: Brezočnik, Z., Kapus, T. (eds.) Proceedings of the COST 247 International Workshop on Applied Formal Methods in System Design, Maribor, Slovenia, pp. 136–145. University of Maribor, Slovenia, June 1996Google Scholar
  75. 75.
    Serwe, W.: Formal specification and verification of fully asynchronous implementations of the data encryption standard. In: van Glabbeek, R., Groote, J.F., Höfner, 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)Google Scholar
  76. 76.
    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–150. IEEE Press, Piscataway, December 1993Google Scholar
  77. 77.
    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–325. IEEE Press, Piscataway, October 1993Google Scholar
  78. 78.
    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 2009Google Scholar
  79. 79.
    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–260. Springer, Heidelberg (2003).  https://doi.org/10.1007/978-3-540-39958-2_17. Full version available as INRIA Research Report RR-5012CrossRefGoogle Scholar
  80. 80.
    Valmari, A.: Compositional state space generation. In: Rozenberg, G. (ed.) ICATPN 1991. LNCS, vol. 674, pp. 427–457. Springer, Heidelberg (1993).  https://doi.org/10.1007/3-540-56689-9_54CrossRefGoogle Scholar
  81. 81.
    Valmari, A.: Compositionality in state space verification methods. In: Billington, J., Reisig, W. (eds.) ICATPN 1996. LNCS, vol. 1091, pp. 29–56. Springer, Heidelberg (1996).  https://doi.org/10.1007/3-540-61363-3_3CrossRefGoogle Scholar
  82. 82.
    Valmari, A.: Composition and abstraction. In: Cassez, F., Jard, C., Rozoy, B., Ryan, M.D. (eds.) MOVEP 2000. LNCS, vol. 2067, pp. 58–98. Springer, Heidelberg (2001).  https://doi.org/10.1007/3-540-45510-8_3CrossRefzbMATHGoogle Scholar
  83. 83.
    Valmari, A., Kemppainen, J., Clegg, M., Levanto, M.: Putting advanced reachability analysis techniques together: The “ARA” tool. In: Woodcock, J.C.P., Larsen, P.G. (eds.) FME 1993. LNCS, vol. 670, pp. 597–616. Springer, Heidelberg (1993).  https://doi.org/10.1007/BFb0024669CrossRefGoogle Scholar
  84. 84.
    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–85. IEEE Computer Society, March 1998Google Scholar
  85. 85.
    Willemse, T.: The specification and validation of the OM/RR-protocol. Master’s thesis, Department of Mathematics and Computing Science, Eindhoven University of Technology, Eindhoven, The Netherlands, June 1998Google Scholar
  86. 86.
    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–344. GMD Report 91, Berlin, April 2000Google Scholar
  87. 87.
    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-PGoogle Scholar
  88. 88.
    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–59. ACM Press, October 1991Google Scholar
  89. 89.
    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–39 (2016)CrossRefGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2018

Authors and Affiliations

  • Hubert Garavel
    • 1
  • Frédéric Lang
    • 1
  • Laurent Mounier
    • 2
  1. 1.Univ. Grenoble Alpes, Inria, CNRS, Grenoble INP, LIGGrenobleFrance
  2. 2.Univ. Grenoble Alpes, CNRS, Grenoble INP, VerimagGrenobleFrance

Personalised recommendations