iBet uBet web content aggregator. Adding the entire web to your favor.
iBet uBet web content aggregator. Adding the entire web to your favor.



Link to original content: https://unpaywall.org/10.1007/S10703-008-0049-6
Learning to divide and conquer: applying the L* algorithm to automate assume-guarantee reasoning | Formal Methods in System Design Skip to main content
Springer Nature Link
Log in

Learning to divide and conquer: applying the L* algorithm to automate assume-guarantee reasoning

  • Published:
Formal Methods in System Design Aims and scope Submit manuscript

Abstract

Assume-guarantee reasoning enables a “divide-and-conquer” approach to the verification of large systems that checks system components separately while using assumptions about each component’s environment. Developing appropriate assumptions used to be a difficult and manual process. Over the past five years, we have developed a framework for performing assume-guarantee verification of systems in an incremental and fully automated fashion. The framework uses an off-the-shelf learning algorithm to compute the assumptions. The assumptions are initially approximate and become more precise by means of counterexamples obtained by model checking components separately. The framework supports different assume-guarantee rules, both symmetric and asymmetric. Moreover, we have recently introduced alphabet refinement, which extends the assumption learning process to also infer assumption alphabets. This refinement technique starts with assumption alphabets that are a subset of the minimal interface between a component and its environment, and adds actions to it as necessary until a given property is shown to hold or to be violated in the system. We have applied the learning framework to a number of case studies that show that compositional verification by learning assumptions can be significantly more scalable than non-compositional verification.

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

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

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

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  1. Alur R, Henzinger T, Mang F, Qadeer S, Rajamani S, Tasiran S (1998) MOCHA: modularity in model checking. In: Proceedings of CAV’98. LNCS, vol 1427. Springer, New York, pp 521–525

    Google Scholar 

  2. Alur R, Cerny P, Madhusudan P, Nam W (2005) Synthesis of interface specifications for Java classes. In: Proceedings of POPL’05, pp 98–109

  3. Alur R, Madhusudan P, Nam W (2005) Symbolic compositional verification by learning assumptions. In: Proceedings of CAV’05. LNCS, vol 3576. Springer, New York, pp 548–562

    Google Scholar 

  4. Angluin D (1987) Learning regular sets from queries and counterexamples. Inf Comput 75(2):87–106

    Article  MATH  MathSciNet  Google Scholar 

  5. Avrunin GS, Corbett JC, Dwyer MB, Păsăreanu CS, Siegel SF (1999) Comparing finite-state verification techniques for concurrent software. TR 99-69, University of Massachusetts, Department of Computer Science, November

  6. Barringer H, Giannakopoulou D, Păsăreanu CS (2003) Proof rules for automated compositional verification through learning. In: Proceedings of SAVCBS’03, pp 14–21

  7. Chaki S, Strichman O (2007) Optimized L*-based assume-guarantee reasoning. In: Proceedings of TACAS’07. LNCS, vol 4424. Springer, New York, pp 276–291

    Google Scholar 

  8. Cheung SC, Kramer J (1999) Checking safety properties using compositional reachability analysis. ACM Trans Softw Eng Methodol 8(1):49–78

    Article  Google Scholar 

  9. Cimatti A, Clarke EM, Giunchiglia E, Giunchiglia F, Pistore M, Roveri M, Sebastiani R, Tacchella A (2002) NuSMV 2: an opensource tool for symbolic model checking. In: Proceedings of CAV’02. LNCS, vol 2404. Springer, New York, pp 359–364

    Google Scholar 

  10. Clarke EM, Long DE, McMillan KL (1989) Compositional model checking. In: Proceedings of LICS’89, pp 353–362

  11. Clarke EM, Grumberg O, Jha S, Lu Y, Veith H (2000) Counterexample-guided abstraction refinement. In: Proceedings of CAV’00. LNCS, vol 1855. Springer, New York, pp 154–169

    Google Scholar 

  12. Clarke EM, Grumberg O, Peled D (2000) Model checking. MIT Press, Cambridge

    Google Scholar 

  13. Cobleigh JM, Giannakopoulou D, Păsăreanu CS (2003) Learning assumptions for compositional verification. In: Proceedings of TACAS’03. LNCS, vol 2619. Springer, New York, pp 331–346

    Google Scholar 

  14. Cobleigh JM, Avrunin GS, Clarke LA (2006) Breaking up is hard to do: an investigation of decomposition for assume-guarantee reasoning. In: Proceedings of ISSTA’06. ACM, New York, pp 97–108

    Google Scholar 

  15. Dwyer MB, Clarke LA, Cobleigh JM, Naumovich G (2004) Flow analysis for verifying properties of concurrent software systems. ACM Trans Softw Eng Methodol 13(4):359–430

    Article  Google Scholar 

  16. Flanagan C, Freund SN, Qadeer S (2002) Thread-modular verification for shared-memory programs. In: Proceedings of ESOP’02, pp 262–277

  17. Gheorghiu M, Giannakopoulou D, Păsăreanu CS (2007) Refining interface alphabets for compositional verification. In: Proceedings of TACAS’07. LNCS, vol 4424. Springer, New York, pp 292–307

    Google Scholar 

  18. Giannakopoulou D, Păsăreanu CS, Barringer H (2005) Component verification with automatically generated assumptions. Autom Softw Eng 12(3):297–320

    Article  Google Scholar 

  19. Grumberg O, Long DE (1991) Model checking and modular verification. In: Proceedings of CONCUR’91, pp 250–265

  20. Helmbold D, Luckham D (1985) Debugging Ada tasking programs. IEEE Softw 2(2):47–57

    Article  Google Scholar 

  21. Henzinger TA, Jhala R, Majumdar R (2005) Permissive interfaces. In: Proceedings of ESEC/SIGSOFT FSE’05, pp 31–40

  22. Jones CB (1983) Specification and design of (parallel) programs. In: Information processing 83: proceedings of the IFIP 9th world congress. IFIP: North-Holland, Amsterdam, pp 321–332

    Google Scholar 

  23. Keller RK, Cameron M, Taylor RN, Troup DB (May 1991) User interface development and software environments: the Chiron-1 system. In: Proceedings of ICSE’91, pp 208–218

  24. Magee J, Kramer J (1999) Concurrency: state models & Java programs. Wiley, New York

    MATH  Google Scholar 

  25. Maier P (2003) Compositional circular assume-guarantee rules cannot be sound and complete. In: Proceedings of FOSSACS

  26. Nam W, Alur R (2006) Learning-based symbolic assume-guarantee reasoning with automatic decomposition. In: Proceedings of ATVA’06. LNCS, vol 4218. Springer, New York

    Google Scholar 

  27. Păsăreanu CS, Giannakopoulou D (2006) Towards a compositional SPIN. In: Proceedings of SPIN’06. LNCS, vol 3925. Springer, New York, pp 234–251

    Google Scholar 

  28. Pnueli A (1984) In transition from global to modular temporal reasoning about programs. Log Models Concurr Syst 13:123–144

    Google Scholar 

  29. Rivest RL, Shapire RE (1993) Inference of finite automata using homing sequences. Inf Comput 103(2):299–347

    Article  MATH  Google Scholar 

  30. Sharygina N, Chaki S, Clarke EM, Sinha N (2005) Dynamic component substitutability analysis. In: Proceedings of FM’05. LNCS, vol 3582. Springer, New York, pp 512–528

    Google Scholar 

  31. Sinha N, Clarke EM (2007) SAT-based compositional verification using lazy learning. In: Proceedings of CAV’07. LNCS, vol 4590. Springer, New York, pp 39–54

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Perot Systems, NASA Ames Research Center, N269-230, Moffett Field, CA, 94035, USA

    Corina S. Păsăreanu

  2. RIACS, NASA Ames Research Center, N269-230, Moffett Field, CA, 94035, USA

    Dimitra Giannakopoulou

  3. Department of Computer Science, University of Toronto, 10 King’s College Road, Toronto, Ontario, Canada, M5S 3G4

    Mihaela Gheorghiu Bobaru

  4. Department of Computer Science, University of Massachusetts, 140 Governor’s Drive, Amherst, MA, 01003, USA

    Jamieson M. Cobleigh

  5. School of Computer Science, University of Manchester, Oxford Road, Manchester, M13 9PL, UK

    Howard Barringer

Authors
  1. Corina S. Păsăreanu
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Dimitra Giannakopoulou
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Mihaela Gheorghiu Bobaru
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Jamieson M. Cobleigh
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Howard Barringer
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Corina S. Păsăreanu.

Additional information

J.M. Cobleigh currently employed by The MathWorks, Inc., 3 Apple Hill Drive, Natick, MA 01760, USA.

Rights and permissions

Reprints and permissions

About this article

Cite this article

Păsăreanu, C.S., Giannakopoulou, D., Bobaru, M.G. et al. Learning to divide and conquer: applying the L* algorithm to automate assume-guarantee reasoning. Form Methods Syst Des 32, 175–205 (2008). https://doi.org/10.1007/s10703-008-0049-6

Download citation

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10703-008-0049-6

Keywords

Search

Navigation