Compositional Verification Using CADP of the ScalAgent Deployment Protocol for Software Components

  • Frédéric Tronel
  • Frédéric Lang
  • Hubert Garavel
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2884)


In this article, we report about the application of the Cadp verification toolbox to check the correctness of an industrial protocol for deploying and configuring transparently a large set of heterogeneous software components over a set of distributed computers/devices. To cope with the intrinsic complexity of this protocol, compositional verification techniques have been used, including incremental minimization and projections over automatically generated interfaces as advocated by Graf & Steffen and Krimm & Mounier. Starting from the Xml description of a configuration of components to be deployed by the protocol, a translator produces a set of Lotos descriptions, μ-calculus formulas, and the corresponding compositional verification scenario to be executed. The approach is fully automated, as formal methods and tool invocations are made invisible to the end-user, who only has to check the verification results for the configuration under study. Due to the use of compositional verification, the approach can scale to large configurations. So far, Lotos descriptions of more than seventy concurrent processes have been verified successfully.


Model Check Parallel Composition Concurrent Process Referential Process Communication Hiding 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. 1.
    Barthe, G., Gurov, D., Huisman, M.: Compositional Verification of Secure Applet Interactions. In: Kutsche, R.-D., Weber, H. (eds.) FASE 2002. LNCS, vol. 2306, pp. 15–32. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  2. 2.
    Brazier, F., Cornelissen, F., Gustavsson, R., Jonker, C.M., Lindeberg, O., Polak, B., Treur, J.: Compositional Design and Verification of a Multi-Agent System for One-to-Many Negotiation. In: Proceedings of the Third International Conference on Multi-Agent Systems ICMAS 1998. IEEE, Los Alamitos (1998)Google Scholar
  3. 3.
    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 Joint International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols, and Protocol Specification, Testing, and Verification FORTE/PSTV 1996, IFIP, Kaiserslautern, Germany, pp. 435–450 (1996); Full version available as INRIA Research Report RR-2958 Google Scholar
  4. 4.
    Cheung, S.C., Kramer, J.: Checking Safety Properties Using Compositional Reachability Analysis. ACM Transactions on Software Engineering and Methodology 8(1), 49–78 (1999)CrossRefGoogle Scholar
  5. 5.
    Corbett, J., Dwyer, M., Hatcliff, J., Pasareanu, C., Robby, S.L., Zheng, H.: Bandera: Extracting Finite-state Models from Java Source Code. In: Proceedings of the 22nd International Conference on Software Engineering ICSE 2000, Limerick, Ireland, pp. 439–448 (June 2000)Google Scholar
  6. 6.
    Cornejo, M.A., Garavel, H., Mateescu, R., de Palma, N.: Specification and Verification of a Dynamic Reconfiguration Protocol for Agent- Based Applications. In: Laurentowski, A., Kosinski, J., Mossurska, Z., Ruchala, R. (eds.) Proceedings of the 3rd IFIP WG 6.1 International Working Conference on Distributed Applications and Interoperable Systems DAIS 2001, IFIP, Krakow, Poland, pp. 229–242 (2001); Full version available as INRIA Research Report RR-4222Google Scholar
  7. 7.
    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); Full version available as INRIA Research Report RR-3352CrossRefGoogle Scholar
  8. 8.
    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, IFIP, Cheju Island, Korea, pp. 377–392 (2001); Full version available as INRIA Research Report RR-4223Google Scholar
  9. 9.
    Garavel, H., Lang, F., Mateescu, R.: An Overview of CADP 2001. European Association for Software Science and Technology (EASST) Newsletter 4, 13–24 (2002) Also Available as INRIA Technical Report RT-0254Google Scholar
  10. 10.
    Giannakopoulou, D., Kramer, J., Cheung, S.C.: Analysing the behaviour of distributed systems using TRACTA. Journal of Automated Software Engineering, Special issue on Automated Analysis of Software 6(1), 7–35 (1999)CrossRefGoogle Scholar
  11. 11.
    Graf, S., Steffen, B., Lüttgen, G.: Compositional Minimization of Finite State Systems using Interface Specifications. Formal Aspects of Computation 8(5), 607–616 (1996)CrossRefzbMATHGoogle Scholar
  12. 12.
    Graf, S., Steffen, B.: Compositional Minimization of Finite State Systems. In: Clarke, E., Kurshan, R.P. (eds.) CAV 1990. LNCS, vol. 531, pp. 186–196. Springer, Heidelberg (1990)CrossRefGoogle Scholar
  13. 13.
    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, Genève (1989)Google Scholar
  14. 14.
    Jia, G., Graf, S.: Verification Experiments on the MASCARA Protocol. In: Dwyer, M.B. (ed.) SPIN 2001. LNCS, vol. 2057, pp. 123–142. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  15. 15.
    Krimm, J.-P., Mounier, L.: Compositional State Space Generation from LOTOS Programs. In: Brinksma, E. (ed.) TACAS 1997. LNCS, vol. 1217. Springer, Heidelberg (1997) Extended version with proofs available as Research Report VERIMAG RR97-01CrossRefGoogle Scholar
  16. 16.
    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)CrossRefGoogle Scholar
  17. 17.
    Leroy, X., Doligez, D., Garrigue, J., Rémy, D., Vouillon, J.: The Objective Caml system (relase 3.06), documentation and user’s manual (2002),
  18. 18.
    Mateescu, R., Sighireanu, M.: Efficient On-the-Fly Model-Checking for Regular Alternation-Free Mu-Calculus. Science of Computer Programming 46(3), 255–281 (2003)MathSciNetCrossRefzbMATHGoogle Scholar
  19. 19.
    de Roever, W.-P., de Boer, F., Hanneman, U., Hooman, J., Lakhnech, Y., Poel, M., Zwiers, J.: Concurrency Verification – Introduction to Compositional and Noncompositional Methods. Cambridge Tracts in Theoretical Computer Science, vol. 54 (2001)Google Scholar
  20. 20.
    Sabnani, K.K., Lapone, A.M., Uyar, M.U.: An Algorithmic Procedure for Checking Safety Properties of Protocols. IEEE Transactions on Communications 37(9), 940–948 (1989)CrossRefGoogle Scholar
  21. 21.
    Visser, W., Havelund, K., Brat, G., Park, S.: Model Checking Programs. In: Ledru, Y. (ed.) Proceedings of the 15th IEEE International Conference on Automated Software Engineering ASE 2000, Grenoble, France, pp. 3–12 (2000)Google Scholar

Copyright information

© IFIP International Federation for Information Processing 2003

Authors and Affiliations

  • Frédéric Tronel
    • 1
  • Frédéric Lang
    • 1
  • Hubert Garavel
    • 1
  1. 1.INRIA Rhône-Alpes / VASYMontbonnotFrance

Personalised recommendations