Compositional reasoning for port-based distributed systems

ABSTRACT

Many distributed systems using IP-based communication protocols consist of chains of components that run concurrently and communicate asynchronously with their neighbours through ports. We present a compositional reasoning method using model checking and theorem proving to verify liveness properties of a communication protocol for chains of connections consisting of an unknown number of components. We outline how our method is used to verify properties of the call protocol of AT&T's Distributed Feature Composition (DFC) architecture.

References

1. N. Amla, E. A. Emerson, and K. S. Namjoshi. Efficient decompositional model-checking for regular timing diagrams. In Correct Hardware Design and Verification Methods, volume 1703 of LNCS, pages 67--81, 1999.]]
2. G. Bond, F. IvanciĆ, N. Klarlund, and R. Trefler. ECLIPSE feature logic analysis. IP-Telephony Workshop, pages 49--56, 2001.]]
3. D. Brand and P. Zafiropulo. On communicating finite-state machines. J. ACM, 30(2):323--342, 1983.]]
4. J. Burch, E. Clarke, and D. Long. Symbolic model checking with partitioned transition relations. In International Conference on Very Large Scale Integration (VLSI), pages 49--58. IFIP Trans., North-Holland, 1991.]]
5. X. Fu, T. Bultan, and J. Su. Conversation protocols: A formalism for specification and verification of reactive electronic services. In Int'l Conf. on Impl. and Application of Automata, number 2759 in LNCS, pages 188--200. Springer, 2003.]]
6. M. J. C. Gordon and T. F. Melham. Introduction to HOL. Cambridge University Press, 1993.]]
7. O. Grumberg and D. E. Long. Model checking and modular verification. ACM Trans. on Prog. Lang. and Sys., 16(3):843--871, 1994.]]
8. T. Henzinger, S. Qadeer, and S. Rajamani. You assume, we guarantee: Methodology and case studies. In Computer-Aided Verification, volume 1427 of LNCS, pages 440--451. Springer-Verlag, 1998.]]
9. G. J. Holzmann. The Spin Model Checker: Primer and Reference Manual. Addison-Wesley, 2003.]]
10. M. Jackson and P. Zave. Distributed feature composition: A virtual architecture for telecommunications services. IEEE Trans. on Soft. Eng., 24(10):831--847, Aug. 1998.]]
11. M. Jackson and P. Zave. The DFC Manual. AT&T Labs, Nov. 2003.]]
12. A. L. Juarez Dominguez. Verification of DFC call protocol correctness criteria. Master's thesis, School of Computer Science, University of Waterloo. May, 2005.]]
13. K.Bhargavan, D. Obradovic, and C. A. Gunter. Formal verification of standards for distance vector routing protocols. Jour. of the ACM, 49(4):538--576, Jul. 2002.]]
14. K. L. McMillan. Verification of infinite state systems by compositional model checking. In Correct Hardware Design and Verification Methods, number 1703 in LNCS, pages 219--233. Springer, 1999.]]
15. A. Pnueli. In transition from global to modular temporal reasoning about programs. In Logic and models of concurrent systems, pages 123--144. Springer, 1985.]]
16. A. Vardhan, K. Sen, M. Viswanathan, and G. Agha. Learning to verify safety properties. In International Conference on Formal Engineering Methods, volume 3308 of LNCS, pages 274--289. Springer, 2004.]]
17. P. Zave. Formal description of telecommunication services in Promela and Z. In 19th International NATO Summer School: Calculational System Design, pages 395--420, 1999.]]

Index Terms

• Software and its engineering

  • Software creation and management

    • Software verification and validation

      • Formal software verification

  • Software organization and properties

    • Software functional properties

      • Formal methods