Skip to main content
SpringerLink
Log in

Assume-Guarantee Reasoning with Local Specifications

  • Conference paper
Formal Methods and Software Engineering (ICFEM 2010)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 6447))

Included in the following conference series:

Abstract

We investigate assume-guarantee reasoning for global specifications consisting of conjunctions of local specifications. We present a sound and complete assume-guarantee rule that permits reasoning about individual modules for local specifications and draws conclusions on global specifications. We illustrate our approach with an example from the field of network congestion control, where different agents are responsible for controlling packet flow across a shared infrastructure. In this context, we derive an assume-guarantee rule for system stability, and show that this rule is valuable to reason about any number of agents, any initial flow configuration, and any topology of bounded degree.

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Abadi, M., Lamport, L.: Conjoining specifications. ACM Transactions on Programming Languages and Systems 17(3), 507–535 (1995)

    Article  Google Scholar 

  2. Alur, R., Henzinger, T.A.: Reactive modules. In: Proc. 11th Annual IEEE Symposium on Logic in Computer Science Logic in Computer Science (LICS 1996), New Brunswick, USA, July 27-30, pp. 207–218 (1996)

    Google Scholar 

  3. Alur, R., Henzinger, T.A., Mang, F., Qadeer, S., Rajamani, S.K., Tasiran, S.: MOCHA: Modularity in model checking. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol. 1427, pp. 521–525. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  4. Barringer, H., Giannakopoulou, D., Păsăreanu, C.S.: Proof rules for automated compositional verification through learning. In: Proc. 2003 Workshop on Specification and Verification of Component-Based Systems (SAVCBS 2003), Helsinki, Finland, September 1-2, pp. 14–21 (2003)

    Google Scholar 

  5. Berezin, S., Campos, S.V.A., Clarke, E.M.: Compositional reasoning in model checking. In: Revisted Lectures from Proc. International Symposium on Compositionality, Bad Malente, Germany, September 8-12, pp. 81–102 (1997)

    Google Scholar 

  6. Cimatti, A., Clarke, E.M., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV 2: An opensource tool for symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  7. Cobleigh, J., Giannakopoulou, D., Păsăreanu, C.: Learning assumptions for compositional verification. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 331–346. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  8. Farzan, A., Chen, Y.F., Clarke, E.M., Tsay, Y.K., Wang, B.Y.: Extending automated compositional verification to the full class of omega-regular languages. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 2–17. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  9. Francez, N., Pnueli, A.: A proof method for cyclic programs. Acta Informatica 9(2), 133–157 (1978)

    Article  MathSciNet  MATH  Google Scholar 

  10. Gheorghiu Bobaru, M., Păsăreanu, C.S., Giannakopoulou, D.: Automated assume-guarantee reasoning by abstraction refinement. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 135–148. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  11. Giannakopoulou, D., Păsăreanu, C.S., Barringer, H.: Assumption generation for software component verification. In: Proc. 17th IEEE International Conference on Automated Software Engineering (ASE 2002), Edinburgh, UK, September 23-27, pp. 3–12 (2002)

    Google Scholar 

  12. Grumberg, O., Long, D.E.: Model checking and modular verification. ACM Transactions on Programming Languages and Systems 16(3), 843–871 (1994)

    Article  Google Scholar 

  13. Henzinger, T.A., Qadeer, S., Rajamani, S.K.: You assume, we guarantee: Methodology and case studies. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol. 1427, pp. 440–451. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  14. Jones, C.B.: Tentative steps toward a development method for interfering programs. ACM Transactions on Programming Languages and Systems 5(4), 596–619 (1983)

    Article  MATH  Google Scholar 

  15. Kelly, F., Voice, T.: Stability of end-to-end algorithms for joint routing and rate control. ACM SIGCOMM Computer Communication Review 35(2), 5–12 (2005)

    Article  Google Scholar 

  16. Kupferman, O., Vardi, M.Y.: An automata-theoretic approach to modular model checking. ACM Transactions on Programming Languages and Systems 22(1), 87–128 (2000)

    Article  MATH  Google Scholar 

  17. Lomuscio, A., Strulo, B., Walker, N., Wu, P.: Model checking optimisation-based congestion control models. In: Proc. 2009 Workshop on Concurrency, Specification, and Programming (CS&P 2009), Kraków-Przegorzały, Poland, September 28-30, pp. 386–397 (2009)

    Google Scholar 

  18. Lomuscio, A., Strulo, B., Walker, N., Wu, P.: Assume-guarantee verification for distributed systems with local specifications. Tech. Rep. RN/10/01, Department of Computer Science, University College London (February 2010)

    Google Scholar 

  19. Low, S.H., Lapsley, D.E.: Optimization flow control, I: basic algorithm and convergence. IEEE/ACM Transactions on Networking 7(6), 861–874 (1999)

    Article  Google Scholar 

  20. Maier, P.: Compositional circular assume-guarantee rules cannot be sound and complete. In: Gordon, A.D. (ed.) FOSSACS 2003. LNCS, vol. 2620, pp. 343–357. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  21. Misra, J., Chandy, K.M.: Proof of networks of processes. IEEE Transactions on Software Engineering SE 7(4), 417–426 (1981)

    Article  MathSciNet  MATH  Google Scholar 

  22. Nam, W., Alur, R.: Learning-based symbolic assume-guarantee reasoning with automatic decomposition. In: Graf, S., Zhang, W. (eds.) ATVA 2006. LNCS, vol. 4218, pp. 170–185. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  23. Nam, W., Madhusudan, P., Alur, R.: Automatic symbolic compositional verification by learning assumptions. Formal Methods in System Design 32(3), 207–234 (2008)

    Article  MATH  Google Scholar 

  24. Păsăreanu, C.S., Giannakopoulou, D., Bobaru, M.G., Cobleigh, J.M., Barringer, H.: Learning to divide and conquer: applying the L* algorithm to automate assume-guarantee reasoning. Formal Methods in System Design 32(3), 175–205 (2008)

    Article  MATH  Google Scholar 

  25. Tsay, Y.K., Chen, Y.F., Tsai, M.H., Wu, K.N., Chan, W.C.: GOAL: A graphical tool for manipulating büchi automata and temporal formulae. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 466–471. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  26. Yuen, C., Tjioe, W.: Modeling and verifying a price model for congestion control in computer networks using promela/spin. In: Dwyer, M.B. (ed.) SPIN 2001. LNCS, vol. 2057, pp. 272–287. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computing, Imperial College London, UK

    Alessio Lomuscio

  2. BT Innovate, Adastral Park, UK

    Ben Strulo & Nigel Walker

  3. State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, China

    Peng Wu

Authors
  1. Alessio Lomuscio
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Ben Strulo
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Nigel Walker
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Peng Wu
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. School of Computing, Computer Science Dept, National University of Singapore, 13 Computing Drive, 117417, Singapore, Singapore

    Jin Song Dong

  2. Software Engineering Institute, East China Normal University, 3663 Zhongshan Road (North), 200062, Shanghai, China

    Huibiao Zhu

Rights and permissions

Reprints and permissions

Copyright information

© 2010 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Lomuscio, A., Strulo, B., Walker, N., Wu, P. (2010). Assume-Guarantee Reasoning with Local Specifications. In: Dong, J.S., Zhu, H. (eds) Formal Methods and Software Engineering. ICFEM 2010. Lecture Notes in Computer Science, vol 6447. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-16901-4_15

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-16901-4_15

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-16900-7

  • Online ISBN: 978-3-642-16901-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation