Skip to main content
SpringerLink
Log in

Compositional verification of asynchronous concurrent systems using CADP

  • Original Article
  • Published:
Acta Informatica Aims and scope Submit manuscript

Abstract

During the last decades, concurrency theory successfully developed salient concepts to formally model and soundly reason about distributed and parallel systems. In practice, however, most attempts at analyzing large systems face severe complexity issues, especially state explosion, which prevents to exhaustively enumerate reachable state spaces. Compositionality is the most promising approach to fight state explosion. In this article, we focus on finite-state verification techniques for asynchronous message-passing systems, highlighting the existence of multiple, diverse compositional techniques such as: compositional model generation, semi-composition and projection, automatic generation of projection interfaces, formula-dependent model generation, and partial model checking. These approaches have been implemented in the framework of the CADP (Construction and Analysis of Distributed Processes) software toolbox and applied to large-scale, industrial systems. A key point is the ability to combine several compositional techniques, as no single technique is sufficient to address all kinds of systems.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Fig. 1
Fig. 2
Fig. 3
Fig. 4
Fig. 5
Fig. 6
Fig. 7

Similar content being viewed by others

Notes

  1. This definition of semi-composition is simpler but equivalent to that given in [83].

  2. This limitation holds similarly for the approach described in [31].

  3. \(\alpha \)-conversion is a well-known equivalence relation between terms that differ only in variable names, originally defined in the framework of the \(\lambda \)-calculus and applied implicitly during substitution to avoid variable capture.

  4. Considering a formula \(\varphi \) in disjunctive form, the sign of variable \(X^k\) is \(\mu \) if \(\varphi [X^k]\) occurs in \(\varphi \) in the context of an even number of negations, and \(\nu \) otherwise.

  5. Note that terms will be compiled into graphs, thus enabling the sharing of sub-formulas that is also possible using equations.

  6. http://www.cs.sunysb.edu/~cwb.

  7. mcrl2.org.

  8. fmt.cs.utwente.nl/tools/ltsmin.

  9. http://cadp.inria.fr.

  10. http://convecs.inria.fr/software/pmc.

  11. http://cadp.inria.fr/man/svl.html.

References

  1. Aceto, L., Fokkink, W., Verhoef, C.: Structural Operational Semantics (Chapter 3), pp. 197–292. North-Holland, Amsterdam (2001)

  2. Ajami, K., Haddad, S., Ilié, J.-M.: Exploiting symmetry in linear time temporal logic model checking: one step beyond. In: Proceedings of Tools and Algorithms for Construction and Analysis of Systems TACAS’98, Lecture Notes in Computer Science, vol. 1384, pp. 52–67. Springer (1998)

  3. Andersen, H.R.: Model checking and boolean graphs. Theoret. Comput. Sci. 126(1), 3–30 (1994)

    Article  MATH  MathSciNet  Google Scholar 

  4. Andersen, H.R.: Partial model checking. In: Proceedings of Logic in Computer Science LICS’95, pp. 398–407. IEEE (1995)

  5. Andersen, H.R., Lind-Nielsen, J.: Partial model checking of modal equations: a survey. J. Softw. Tools Technol. Transf. 2, 242–259 (1999)

    Article  MATH  Google Scholar 

  6. Andersen, H.R., Staunstrup, J., Maretti, N.: A comparison of modular verification techniques. In: Proceedings of CAAP/FASE’97, Lecture Notes in Computer Science, vol. 1214. Springer (1997)

  7. Andersen, H.R., Staunstrup, J., Maretti, N.: Partial model checking with robdds. In: Proceedings of Tools and Algorithms for Construction and Analysis of Systems TACAS’97, Lecture Notes in Computer Science, vol. 1217. Springer (1997)

  8. Andersen, H.R., Winskel, G.: Compositional checking of satisfaction. In: Proceedings of Computer Aided Verification CAV’91, Lecture Notes in Computer Science, vol. 575, pp. 24–36. Springer (1991)

  9. Armoni, R., Fix, L., Flaisher, A., Gerth, R., Ginsburg, B., Kanza, T., Landver, A., Mador-Haim, S., Singerman, E., Tiemeyer, A., Vardi, M.Y., Zbar, Y.: The ForSpec temporal logic: a new temporal property-specification language. In: Proceedings of Tools and Algorithms for the Construction and Analysis of Systems TACAS’02, Lecture Notes in Computer Science, vol. 2280, pp. 296–211. Springer (2002)

  10. Armstrong, P.J., Goldsmith, M., Lowe, G., Ouaknine, J., Palikareva, H., Roscoe, A.W., Worrell, J.: Recent developments in FDR. In: Proceedings of Computer Aided Verification CAV’12, Lecture Notes in Computer Science, vol. 7358, pp. 699–704. Springer (2012)

  11. Arnold, A.: MEC: a system for constructing and analysing transition systems. In: Proceedings of Automatic Verification Methods for Finite State Systems CAV’89, Lecture Notes in Computer Science, vol. 407, pp. 117–132. Springer (1989)

  12. Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, Cambridge (2008)

    MATH  Google Scholar 

  13. Barbuti, R., de Francesco, N., Santone, A., Vaglini, G.: Selective mu-calculus and formula-based equivalence of transition systems. J. Comput. Syst. Sci. 59(3), 537–556 (1999)

    Article  MATH  Google Scholar 

  14. Barringer, H., Goldberg, A., Havelund, K., Sen, K.: Rule-based runtime verification. In: Proceedings of Verification, Model Checking, and Abstract Interpretation VMCAI’04, Lecture Notes in Computer Science, vol. 2937, pp. 44–57. Springer (2004)

  15. Basu, S., Ramakrishnan, C.R.: Compositional analysis for verification of parameterized systems. In: Proceedings of Tools and Algorithms for the Construction and Analysis of Systems TACAS’03, Lecture Notes in Computer Science, vol. 2619, pp. 315–330. Springer (2003)

  16. Beer, I., Ben-David, S., Landver, A.: On-the-fly model checking of RCTL formulas. In: Proceedings of Computer Aided Verification CAV’98, Lecture Notes in Computer Science, vol. 1427, pp. 184–194. Springer (1998)

  17. Berard, B., Laroussinie, F.: Verification compositionnelle des p-automates. Technical Report Lot 4.1, Réseau National des Technologies Logicielles, Project AVERROES (2003)

  18. Bergstra, J.A., Klop, J.W.: Algebra of communicating processes with abstraction. Theoret. Comput. Sci. 37, 77–121 (1985)

    Article  MATH  MathSciNet  Google Scholar 

  19. Bergstra, J.A., Ponse, A., Smolka, S.A. (eds.): Handbook of Process Algebra. Elsevier, Amsterdam (2001)

    MATH  Google Scholar 

  20. Blom, S., Orzan, S.: Distributed state space minimization. Softw. Tools Technol. Transf. 7(3), 280–291 (2005)

    Article  Google Scholar 

  21. Blom, S., van de Pol, J., Weber, M.: LTSmin: distributed and symbolic reachability. In: Proceedings of Computer Aided Verification CAV’10, Lecture Notes in Computer Science, vol. 6174, pp. 354–359. Springer (2010)

  22. Bodentien, N., Vestergaard, J., Friis, J., Kristoffersen, K., Larsen, K.G.: Verification of state/event systems by quotienting. Technical Report RS-99-41, Basic Research in Computer Science (1999)

  23. Bouajjani, A., Fernandez, J.-C., Graf, S., Rodríguez, C., Sifakis, J.: Safety for branching time semantics. In: Proceedings of ICALP. Springer (1991)

  24. Bouali, A., Ressouche, A., Roy, V., de Simone, R.: The fc2tools set: a toolset for the verification of concurrent systems. In: Proceedings of Computer-Aided Verification CAV’96, Lecture Notes in Computer Science, vol. 1102. Springer (1996)

  25. Bradfield, J.C., Stirling, C.: Modal Logics and Mu-Calculi: An Introduction (Chapter 4). Elsevier, Amsterdam (2001)

    Book  Google Scholar 

  26. Brookes, S.D., Hoare, C.A.R., Roscoe, A.W.: A theory of communicating sequential processes. J. ACM 31(3), 560–599 (1984)

    Article  MATH  MathSciNet  Google Scholar 

  27. Cassez, F., Laroussinie, F.: Model-checking for hybrid systems by quotienting and constraints solving. In: Proceedings of Computer Aided Verification CAV’00, Lecture Notes in Computer Science, vol. 1855. Springer (2000)

  28. Champelovier, D., Clerc, X., Garavel, H., Guerte, Y., McKinty, C., Powazny, V., Lang, F., Serwe, W., Smeding, G.: Reference Manual of the LNT to LOTOS Translator (Version 6.1). INRIA/VASY and INRIA/CONVECS (2014)

  29. 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: Proceedings of Formal Description Techniques for Distributed Systems and Communication Protocols / Protocol Specification, Testing, and Verification FORTE/PSTV’96, pp. 435–450. IFIP, Chapman & Hall (1996)

  30. Cheung, K.H.: Compositional Analysis of Complex Distributed Systems. PhD thesis, Department of Computer Science, Hong Kong University of Science and Technology, Hong Kong (1998)

  31. Cheung, S.C., Kramer, J.: Enhancing compositional reachability analysis with context constraints. In: Proceedings of Foundations of Software Engineering, pp. 115–125. ACM Press (1993)

  32. Cheung, S.C., Kramer, J.: Compositional reachability analysis of finite-state distributed systems with user-specified constraints. In: Proceedings of Foundations of Software Engineering, pp. 140–150. ACM Press (1995)

  33. Cheung, S.C., Kramer, J.: Context constraints for compositional reachability. ACM Trans. Softw. Eng. Methodol. 5(4), 334–377 (1996)

    Article  Google Scholar 

  34. Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (2000)

    Google Scholar 

  35. Clarke, E.M., Emerson, E.A., Jha, S., Prasad Sistla, A.: Symmetry reductions in model checking. In: Proceedings of Computer Aided Verification CAV’98, Lecture Notes in Computer Science, vol. 1427, pp. 147–158. Springer (1998)

  36. Clarke, E.M., Jha, S., Enders, R., Filkorn, T.: Exploiting symmetry in temporal logic model checking. Form. Methods Syst. Des. 9(1/2), 77–104 (1996)

    Article  Google Scholar 

  37. Cleaveland, R., Parrow, J., Steffen, B.: The concurrency workbench. In: Proceedings of Automatic Verification Methods for Finite State Systems, Lecture Notes in Computer Science, vol. 407, pp. 24–37. Springer (1989)

  38. Cleaveland, R., Steffen, B.: A linear-time model-checking algorithm for the alternation-free modal mu-calculus. Form. Methods Syst. Des. 2(2), 121–147 (1993)

    Article  MATH  Google Scholar 

  39. Coste, N., Garavel, H., Hermanns, H., Lang, F., Mateescu, R., Serwe, W.: Ten years of performance evaluation for concurrent systems using CADP. In: Proceedings of Leveraging Applications of Formal Methods, Verification and Validation ISoLA’10, Lecture Notes in Computer Science, vol. 6416, pp. 128–142. Springer (2010)

  40. Crouzen, P., Hermanns, H.: Aggregation ordering for massively parallel compositional models. In: Proceedings of Application of Concurrency to System Design ACSD’10. IEEE (2010)

  41. Crouzen, P., Lang, F.: Smart reduction. In: Proceedings of Fundamental Approaches to Software Engineering FASE’2011, Lecture Notes in Computer Science, vol. 6603, pp. 111–126. Springer (2011)

  42. Dam, M.: Model checking mobile processes. In: Proceedings of Concurrency Theory CONCUR’93, Lecture Notes in Computer Science, vol. 715, pp. 22–36. Springer (1993)

  43. Du, X., Smolka, S.A., Cleaveland, R.: Local model checking and protocol analysis. J. Softw. Tools Technol. Transf. 2(3), 219–241 (1999)

    Article  MATH  Google Scholar 

  44. Emerson, E.A., Clarke, E.M.: Using branching time logic to synthesize synchronization skeletons. Sci. Comput. Program. 2, 241–266 (1982)

    Article  MATH  Google Scholar 

  45. Emerson, E.A., Halpern, J.Y.: “Sometimes” and “not never” revisited: on branching versus linear time temporal logic. J. ACM 33(1), 151–178 (1986)

    Article  MATH  MathSciNet  Google Scholar 

  46. Emerson, E.A., Lei, C.-L.: Efficient model checking in fragments of the propositional mu-calculus. In: Proceedings of Logic in Computer Science LICS’86, pp. 267–278 (1986)

  47. Fantechi, A., Gnesi, S., Ristori, G.: From actl to mu-calculus. In: Proceedings of Theory and Practice in Verification. IEI-CNR, pp. 3–10 (1992)

  48. Fantechi, A., Gnesi, S., Ristori, G.: Model checking for action-based logics. Form. Methods Syst. Des. 4, 187–203 (1994)

    Article  MATH  Google Scholar 

  49. Fernandez, J.-C.: ALDEBARAN : un système de vérification par réduction de processus communicants. Thèse de Doctorat, Université Joseph Fourier (Grenoble) (1988)

  50. Fernandez, J.-C., Garavel, H., Mounier, L., Rasse, A., Rodríguez, C., Sifakis, J.: A toolbox for the verification of lotos programs. In: Proceedings of Software Engineering ICSE’14, pp. 246–259. ACM (1992)

  51. Fernandez, J.-C., Mounier, L.: “on the fly” verification of behavioural equivalences and preorders. In: Proceedings of Computer-Aided Verification CAV’91, Lecture Notes in Computer Science, vol. 575, pp. 181–191. Springer (1991)

  52. Fernandez, J.-C., Mounier, L.: A tool set for deciding behavioral equivalences. In: Proceedings of CONCUR’91 (1991)

  53. Fischer, M.J., Ladner, R.E.: Propositional dynamic logic of regular programs. J. Comput. Syst. Sci. 18(2), 194–211 (1979)

    Article  MATH  MathSciNet  Google Scholar 

  54. Flanagan, C., Godefroid, P.: Dynamic partial-order reduction for model checking software. In: Proceedings of Principles of Programming Languages POPL’05. ACM Press (2005)

  55. Garavel, H.: Compilation of lotos abstract data types. In: Proceedings of Formal Description Techniques FORTE’89, pp. 147–162. North-Holland (1989)

  56. Garavel, H.: Open/cæsar: an open software architecture for verification, simulation, and testing. In: Proceedings of Tools and Algorithms for the Construction and Analysis of Systems TACAS’98, Lecture Notes in Computer Science, vol. 1384, pp. 68–84. Springer (1998)

  57. Garavel, H., Lang, F.: Svl: a scripting language for compositional verification. In: Proceedings of Formal Techniques for Networked and Distributed Systems FORTE’2001, pp. 377–392. IFIP, Kluwer (2001)

  58. Garavel, H., Lang, F., Mateescu, R., Serwe, W.: Cadp 2010: A toolbox for the construction and analysis of distributed processes. In: Proceedings of Tools and Algorithms for the Construction and Analysis of Systems TACAS’2011, Lecture Notes in Computer Science, vol. 6605, pp. 372–387 (2011)

  59. Garavel, H., Salaün, G., Serwe, W.: On the semantics of communicating hardware processes and their translation into LOTOS for the verification of asynchronous circuits with CADP. Sci. Comput. Program. 74(3), 100–127 (2009)

    Article  MATH  Google Scholar 

  60. Garavel, H., Sifakis, J.: Compilation and verification of LOTOS specifications. In: Proceedings of Protocol Specification, Testing and Verification PSTV’90, pp. 379–394. IFIP, North-Holland (1990)

  61. Garavel, H., Sighireanu, M.: A graphical parallel composition operator for process algebras. In: Proceedings of Formal Description Techniques for Distributed Systems and Communication Protocols/Protocol Specification, Testing, and Verification FORTE/PSTV’99, pp. 185–202. IFIP, Kluwer (1999)

  62. Garavel, H., Thivolle, D.: Verification of gals systems by combining synchronous languages and process calculi. In: Proceedings of Model Checking Software SPIN’2009, Lecture Notes in Computer Science, vol. 5578, pp. 241–260. Springer (2009)

  63. Giannakopoulou, D.: Model Checking for Concurrent Software Architectures. PhD thesis, Imperial College of Science, Technology and Medicine, University of London (1999)

  64. Giannakopoulou, D., Magee, J.: Fluent model checking for event-based systems. In: Proceedings of Foundations of Software Engineering ESEC/FSE’2003, pp. 257–266. ACM (2003)

  65. Gibson-Robinson, T., Armstrong, P.J., Boulgakov, A., Roscoe, A.W.: FDR3—A modern refinement checker for CSP. In: Proceedings of Tools and Algorithms for the Construction and Analysis of Systems TACAS’14, Lecture Notes in Computer Science, vol. 8413, pp. 187–201. Springer (2014)

  66. Godefroid, P.: Using partial orders to improve automatic verification methods. In: Proceedings of Computer-Aided Verification CAV’90, DIMACS Series in Discrete Mathematics and Theoretical Computer Science, vol. 3, pp. 321–340. AMS-ACM (1990)

  67. Godefroid, P., Wolper, P.: A partial approach to model checking. In: Proceedings of Logic in Computer Science LICS’91. IEEE (1991)

  68. Godefroid, P., Wolper, P.: Using partial orders for the efficient verification of deadlock freedom and safety properties. In: Proceedings of Computer-Aided Verification CAV’91, Lecture Notes in Computer Science, vol. 575. Springer (1991)

  69. Graf, S., Steffen, B.: Compositional minimization of finite state systems. In: Proceedings of Computer-Aided Verification CAV’90, Lecture Notes in Computer Science, vol. 531, pp. 186–196. Springer (1990)

  70. Graf, S., Steffen, B., Lüttgen, G.: Compositional minimisation of finite state systems using interface specifications. Form. Aspects Comput. 8(5), 607–616 (1996)

    Article  MATH  Google Scholar 

  71. Groote, J.F., Kouters, T.W.D.M., Osaiweran, A.A.H.: Specification guidelines to avoid the state space explosion problem. J. Softw. Test. Verif. Reliab. 25(1), 4–33 (2015) (2014)

  72. Groote, J.F., Ponse, A.: The syntax and semantics of \(\mu \)CRL. In: Proceedings of Workshop on the Algebra of Communicating Processes ACP’94, Workshops in Computing Series, pp. 26–62. Springer (1995)

  73. Groote, J.F., Vaandrager, F.: An efficient algorithm for branching bisimulation and stuttering equivalence. In: Proceedings of ICALP’90, Lecture Notes in Computer Science, vol. 443, pp. 626–638. Springer (1990)

  74. Halbwachs, N.: Synchronous Pogramming of Reactive Systems. Kluwer, Amsterdam (1993)

    Book  Google Scholar 

  75. Hamaguchi, K., Hiraishi, H., Yajima, S.: Branching time regular temporal logic for model checking with linear time complexity. In: Proceedings of Computer Aided Verification CAV’90, Lecture Notes in Computer Science, vol. 531, pp. 253–262. Springer (1990)

  76. Hennessy, M.: The semantics of programming languages: an elementary introduction using structural operational semantics. Wiley, New York (1990)

    MATH  Google Scholar 

  77. Hoare, C.A.R.: Communicating sequential processes. Commun. ACM 21(8), 666–677 (1978)

    Article  MATH  MathSciNet  Google Scholar 

  78. Ip, C.N., Dill, D.L.: Better verification through symmetry. Form. Methods Syst. Des. 9(1/2), 41–75 (1996)

    Google Scholar 

  79. 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 (1989)

  80. ISO/IEC: Enhancements to LOTOS (E-LOTOS). International Standard 15437:2001, International Organization for Standardization—Information Technology (2001)

  81. Katz, S., Peled, D.: An efficient verification method for parallel and distributed programs. In: Proceedings of Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, Lecture Notes in Computer Science, vol. 354, pp. 489–507. Springer (1988)

  82. Kozen, D.: Results on the propositional \(\mu \)-calculus. Theoret. Comput. Sci. 27, 333–354 (1983)

    Article  MATH  MathSciNet  Google Scholar 

  83. Krimm, J.-P., Mounier, L.: Compositional state space generation from lotos programs. In: Proceedings of Tools and Algorithms for the Construction and Analysis of Systems TACAS’97, Lecture Notes in Computer Science, vol. 1217. Springer (1997)

  84. Lang, F.: Compositional verification using svl scripts. In: Proceedings of Tools and Algorithms for the Construction and Analysis of Systems TACAS’2002, Lecture Notes in Computer Science, vol. 2280, pp. 465–469. Springer (2002)

  85. Lang, F.: Exp.open 2.0: A flexible tool integrating partial order, compositional, and on-the-fly verification methods. In: Proceedings of Integrated Formal Methods IFM’2005, Lecture Notes in Computer Science, vol. 3771, pp. 70–88. Springer (2005)

  86. Lang, F.: Refined interfaces for compositional verification. In: Proceedings of Formal Techniques for Networked and Distributed Systems FORTE’2006, Lecture Notes in Computer Science, vol. 4229, pp. 159–174. Springer (2006)

  87. Lang, F., Mateescu, R.: Partial model checking using networks of labelled transition systems and boolean equation systems. In: Proceedings of Tools and Algorithms for the Construction and Analysis of Systems TACAS’2012, Lecture Notes in Computer Science, vol. 7214, pp. 141–156. Springer (2012)

  88. Lang, F., Mateescu, R.: Partial model checking using networks of labelled transition systems and boolean equation systems. Log. Methods Comput. Sci. 9(4), 1–32 (2013)

    MathSciNet  Google Scholar 

  89. Lang, F., Salaün, G., Hérilier, R., Kramer, J., Magee, J.: Translating fsp into lotos and networks of automata. Form. Aspects Comput. 22(6), 681–711 (2010)

    Article  MATH  Google Scholar 

  90. Laroussinie, F., Larsen, K.G.: Compositional model checking of real time systems. In: Proceedings of Concurrency Theory CONCUR’95, Lecture Notes in Computer Science, vol. 962. Springer (1995)

  91. Laroussinie, F., Larsen, K.G.: Cmc: A tool for compositional model checking of real-time systems. In: Proceedings of Formal Description Techniques for Distributed Systems and Communication Protocols/Protocol Specification, Testing and Verification FORTE/PSTV’98, IFIP Conference Proceedings, vol. 135. Kluwer (1998)

  92. Larsen, K.G.: Proof systems for Hennessy-Milner logic with recursion. In: Proceedings of Trees in Algebra and Programming CAAP’88, Lecture Notes in Computer Science, vol. 299, pp. 215–230. Springer (1988)

  93. Larsen, K.G., Pettersson, P., Yi, W.: Compositional and symbolic model checking of real-time systems. In: Proceedings of Real-Time Systems. IEEE (1995)

  94. Magee, J., Kramer, J.: Concurrency: State Models and Java Programs, 2006th edn. Wiley, New York (2006)

    Google Scholar 

  95. Malhotra, J., Smolka, S.A., Giacalone, A., Shapiro, R.: A tool for hierarchical design and simulation of concurrent systems. In: Proceedings of Specification and Verification of Concurrent Systems, pp. 140–152. British Computer Society (1988)

  96. Manna, Z., Pnueli, A.: A hierarchy of temporal properties. In: Proceedings of Principles of Distributed Computing PODC’90, pp. 377–408 (1990)

  97. Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems, vol. I (Specification). Springer (1992)

  98. Martin, A.J.: Compiling communicating processes into delay-insensitive VLSI circuits. Distrib. Comput. 1(4), 226–234 (1986)

    Article  MATH  Google Scholar 

  99. Martinelli, F.: Symbolic partial model checking for security analysis. In: Proceedings of Mathematical Methods, Models, and Architectures for Computer Network Security MMM-ACNS, Lecture Notes in Computer Science, vol. 2776. Springer (2003)

  100. Mateescu, R.: Local model-checking of an alternation-free value-based modal mu-calculus. In: Proceedings ofVerification, Model Checking and Abstract Interpretation VMCAI’98. University Ca’ Foscari of Venice (1998)

  101. Mateescu, R.: Efficient diagnostic generation for boolean equation systems. In: Proceedings of Tools and Algorithms for the Construction and Analysis of Systems TACAS’2000, Lecture Notes in Computer Science, vol. 1785, pp. 251–265. Springer (2000)

  102. Mateescu, R.: Caesar\_solve: a generic library for on-the-fly resolution of alternation-free boolean equation systems. J. Softw. Tools Technol. Transf. 8(1), 37–56 (2006)

    Article  MathSciNet  Google Scholar 

  103. Mateescu, R., Salaün, G.: Translating pi-calculus into LOTOS NT. In: Proceedings of Integrated Formal Methods IFM’2010, Lecture Notes in Computer Science, vol. 6396, pp. 229–244. Springer (2010)

  104. Mateescu, R., Sighireanu, M.: Efficient on-the-fly model-checking for regular alternation-free mu-calculus. Sci. Comput. Program. 46(3), 255–281 (2003)

    Article  MATH  MathSciNet  Google Scholar 

  105. Mateescu, R., Thivolle, D.: A model checking language for concurrent value-passing systems. In: Proceedings of Formal Methods FM’08, Lecture Notes in Computer Science, vol. 5014, pp. 148–164. Springer (2008)

  106. Mateescu, R., Wijs, A.: Property-dependent reductions adequate with divergence-sensitive branching bisimilarity. Sci. Comput. Program. 96(3), 354–376 (2014)

    Article  Google Scholar 

  107. Milner, R.: A Calculus of Communicating Systems, Lecture Notes in Computer Science, vol. 92. Springer (1980)

  108. Milner, R.: Communication and Concurrency. Prentice-Hall, Upper Saddle River (1989)

    MATH  Google Scholar 

  109. Milner, R.: Communicating and Mobile Systems: The Pi-Calculus. Cambridge University Press, Cambridge (1999)

    MATH  Google Scholar 

  110. Müller-Olm, M., Schmidt, D., Steffen, B.: Model-checking: a tutorial introduction. In: Proceedings of Static Analysis Symposium SAS’99, Lecture Notes in Computer Science, vol. 1694, pp. 330–354. Springer (1999)

  111. De Nicola, R., Fantechi, A., Gnesi, S., Ristori, G.: An action-based framework for verifying logical and behavioural properties of concurrent systems. In: Proceedings of Computer Aided Verification CAV’91, Lecture Notes in Computer Science, vol. 575, pp. 37–47. Springer (1991)

  112. De Nicola, R., Vaandrager, F.W.: Action Versus State Based Logics for Transition Systems, Lecture Notes in Computer Science, vol. 469, pp. 407–419. Springer (1990)

  113. Osaiweran, A.A.H.: Formal Development of Control Software in the Medical Systems Domain. PhD thesis, Eindhoven University of Technology (2012)

  114. Overman, W.T., Crocker, S.D.: Verification of concurrent systems: function and timing. In: Proceedings of Protocol Specification, Testing and Verification PSTV’82, pp. 401–409. North-Holland (1982)

  115. Paige, R., Tarjan, R.E.: Three partition refinement algorithms. SIAM J. Comput. 16(6), 973–989 (1987)

    Article  MATH  MathSciNet  Google Scholar 

  116. Park, D.: Concurrency and automata on infinite sequences. In: Theoretical Computer Science, Lecture Notes in Computer Science, vol. 104, pp. 167–183. Springer (1981)

  117. Peled, D.: All from one, one for all: on model checking using representatives. In: Proceedings of Computer Aided Verification CAV’93, Lecture Notes in Computer Science, vol. 697, pp. 409–423. Springer (1993)

  118. Plotkin, G.D.: A Structural Approach to Operational Semantics. Report DAIMI FN-19, Computer Science Department, Aarhus University (1981)

  119. Plotkin, G.D.: A structural approach to operational semantics. J. Log. Algebr. Program. 60–61, 17–139 (2004)

    MathSciNet  Google Scholar 

  120. Plotkin, G.D.: The origins of structural operational semantics. J. Log. Algebr. Program. 60–61, 3–15 (2004)

    Article  MathSciNet  Google Scholar 

  121. Pnueli, A.: The temporal logic of programs. In: Proceedings of Foundations of Computer Science, pp. 46–57. IEEE (1977)

  122. Pnueli, A.: A temporal logic of concurrent programs. Theoret. Comput. Sci. 13, 45–60 (1981)

    Article  MATH  MathSciNet  Google Scholar 

  123. Queille, J.-P., Sifakis, J.: Fairness and related properties in transition systems—a temporal logic to deal with fairness. Acta Inf. 19, 195–220 (1983)

    Article  MATH  MathSciNet  Google Scholar 

  124. Rathke, J., Hennessy, M.: Local Model Checking for a Value-Based Modal \(\mu \)-Calculus. Report 5/96, School of Cognitive and Computing Sciences, University of Sussex (1996)

  125. Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice Hall, Upper Saddle River (1998)

    Google Scholar 

  126. 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)

    Article  Google Scholar 

  127. Streett, R.: Propositional dynamic logic of looping and converse. Inf. Control 54, 121–141 (1982)

    Article  MATH  MathSciNet  Google Scholar 

  128. Tai, K.C., Koppol, V.: Hierarchy-based incremental reachability analysis of communication protocols. In: Proceedings of Network Protocols, pp. 318–325. IEEE (1993)

  129. Tai, K.C., Koppol, V.: An incremental approach to reachability analysis of distributed programs. In: Proceedings of Software Specification and Design, pp. 141–150. IEEE Press (1993)

  130. Thivolle, D.: Langages modernes pour la vérification des systèmes asynchrones. Thèse de Doctorat, Université Joseph Fourier (Grenoble, France) and Universitatea Politehnica din Bucuresti (Bucharest, Romania) (2011)

  131. Thomas, W.: Computation Tree Logic and Regular \(\omega \)-Languages, Lecture Notes in Computer Science, vol. 354, pp. 690–713 (1989)

  132. Tronel, F., Lang, F., Garavel, H.: Compositional verification using cadp of the scalagent deployment protocol for software components. In: Proceedings of Formal Methods for Open Object-based Distributed Systems FMOODS’2003, Lecture Notes in Computer Science, vol. 2884, pp. 244–260. Springer (2003)

  133. Valmari, A.: A stubborn attack on state explosion. In: Proceedings of Computer-Aided Verification CAV’90, DIMACS Series in Discrete Mathematics and Theoretical Computer Science, vol. 3, pp. 25–42. AMS-ACM (1990)

  134. Valmari, A.: Compositional state space generation. In: Proceedings of Advances in Petri Nets, Lecture Notes in Computer Science, vol. 674, pp. 427–457. Springer (1993)

  135. van Glabbeek, R.J.: The Linear Time-Branching Time Spectrum I. The Semantics of Concrete, Sequential Processes (Chapter 1), pp. 3-99. North-Holland, Amsterdam (2001)

  136. van Glabbeek, R.J., Weijland, W.P.: Branching-time and abstraction in bisimulation semantics (extended abstract). CS R8911, Centrum voor Wiskunde en Informatica (1989)

  137. van Glabbeek, R.J., Weijland, W.P.: Branching-time and abstraction in bisimulation semantics. J. ACM 43(3), 555–600 (1996)

    Article  MATH  MathSciNet  Google Scholar 

  138. Wolper, P.: Temporal logic can be more expressive. Inf. Control 56(1/2), 72–99 (1983)

    Article  MATH  MathSciNet  Google Scholar 

  139. Yeh, W.J.: Controlling State Explosion in Reachability Analysis. PhD thesis, Software Engineering Research Center (SERC) Laboratory, Purdue University, (1993). Technical Report SERC-TR-147-P

  140. Yeh, W.J., Young, M.: Compositional reachability analysis using process algebra. In: Proceedings of Testing, Analysis, and Verification SIGSOFT’91, pp. 49–59. ACM Press (1991)

Download references

Author information

Authors and Affiliations

  1. Inria, Grenoble, France

    Hubert Garavel, Frédéric Lang & Radu Mateescu

  2. Université Grenoble Alpes, LIG, 38000, Grenoble, France

    Hubert Garavel, Frédéric Lang & Radu Mateescu

  3. CNRS, LIG, 38000, Grenoble, France

    Hubert Garavel, Frédéric Lang & Radu Mateescu

Authors
  1. Hubert Garavel
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Frédéric Lang
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Radu Mateescu
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Hubert Garavel.

Rights and permissions

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Garavel, H., Lang, F. & Mateescu, R. Compositional verification of asynchronous concurrent systems using CADP. Acta Informatica 52, 337–392 (2015). https://doi.org/10.1007/s00236-015-0226-1

Download citation

  • Received:

  • Accepted:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s00236-015-0226-1

Search

Navigation