×

zbMATH — the first resource for mathematics

Three optimizations for assume-guarantee reasoning with \(L^{*}\). (English) Zbl 1147.68569
Summary: The learning-based automated Assume-Guarantee reasoning paradigm has been applied in the last few years for the compositional verification of concurrent systems. Specifically, \(L^{*}\) has been used for learning the assumption, based on strings derived from counterexamples, which are given to it by a model-checker that attempts to verify the Assume-Guarantee rules. We suggest three optimizations to this paradigm. First, we derive from each counterexample multiple strings to \(L^{*}\), rather than a single one as in previous approaches. This small improvement saves candidate queries and hence model-checking runs. Second, we observe that in existing instances of this paradigm, the learning algorithm is coupled weakly with the teacher. Thus, the learner completely ignores the details of the internal structure of the system and specification being verified, which are available already to the teacher. We suggest an optimization that uses this information in order to avoid many unnecessary membership queries (it reduces the number of such queries by more than an order of magnitude). Finally, we develop a method for minimizing the alphabet used by the assumption, which reduces the size of the assumption and the number of queries required to construct it. We present these three optimizations in the context of verifying trace containment for concurrent systems composed of finite state machines. We have implemented our approach in the comfort tool, and experimented with real-life examples. Our results exhibit an average speedup of between 4 to 11 times, depending on the Assume-Guarantee rule used and the set of activated optimizations.

MSC:
68Q60 Specification and verification (program logics, model checking, etc.)
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
68Q32 Computational learning theory
Software:
ComFoRT; PBS
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Aloul F, Ramani A, Markov I, Sakallah K (2002) PBS: A backtrack search pseudo-boolean solver and optimizer. In: Proceedings of the 5th international symposium on the theory and applications of satisfiability testing (SAT ’02), Cincinnati, OH, May 6–9, 2002. University of Cincinnati, Cincinnati, pp 346–353. http://gauss.ececs.uc.edu/Conferences/SAT2002/sat2002list.html
[2] Alur R, Cerny P, Gupta G, Madhusudan P, Nam W, Srivastava A (2005) Synthesis of interface specifications for Java classes. In: Palsberg J, Abadi M (eds) Popl05, Long Beach, CA, January 12–14, 2005. Association for Computing Machinery, New York, pp 98–109 · Zbl 1369.68126
[3] Alur R, Madhusudan P, Nam W (2005) Symbolic compositional verification by learning assumptions. In: Etessami K, Rajamani SK (eds) Proceedings of the 17th international conference on computer aided verification (CAV ’05), Edinburgh, Scotland, July 6–10, 2005. Lecture notes in computer science, vol 3576. Springer, New York, pp 548–562 · Zbl 1081.68601
[4] Angluin D (1987) Learning regular sets from queries and counterexamples. Inf Comput 75(2):87–106 · Zbl 0636.68112 · doi:10.1016/0890-5401(87)90052-6
[5] Ball T, Rajamani SK (2002) Generating abstract explanations of spurious counterexamples in C programs. Technical report MSR-TR-2002-09, Microsoft Research, Redmond, Washington, USA, January 2002
[6] Barringer H, Giannakopoulou D, Păsăreanu CS (2003) Proof rules for automated compositional verification. In: Proceedings of the 2nd workshop on specification and verification of component based systems (SAVCBS ’03), Helsinki, Finland, September 1–2, 2003. Iowa State University, Ames, pp 14–21
[7] Chaki S, Clarke EM, Sinha N, Thati P (2005) Automated Assume–Guarantee reasoning for simulation conformance. In: Etessami K, Rajamani SK (eds) Proceedings of the 17th international conference on computer aided verification (CAV ’05), Edinburgh, Scotland, July 2005. Lecture notes in computer science, vol 3576. Springer, Berlin, pp 534–547 · Zbl 1081.68612
[8] Chaki S, Ivers J, Sharygina N, Wallnau K (2005) The ComFoRT reasoning framework. In: Etessami K, Rajamani SK (eds) Proceedings of the 17th international conference on computer aided verification (CAV ’05), Edinburgh, Scotland, July 6–10, 2005. Lecture notes in computer science, vol 3576. Springer, New York, pp 164–169 · Zbl 1081.68613
[9] Chaki S, Sinha N (2006) Assume–Guarantee reasoning for deadlock. In: Proc. of FMCAD, 2006
[10] Chaki S, Strichman O (2006) Optimized L* for Assume–Guarantee reasoning. In: Grumberg O, Huth M (eds) Proceedings of the 13th international conference on tools and algorithms for the construction and analysis of systems (TACAS ’07), Braga, Portugal, March 24–April 1, 2007. Lecture notes in computer science, vol 4424. Springer, New York, pp 276–291
[11] Clarke EM, Grumberg O, Jha S, Lu Y, Veith H (2003) Counterexample-guided abstraction refinement for symbolic model checking. J Assoc Comput Mach 50(5):752–794 · Zbl 1325.68145
[12] Cobleigh JM, Giannakopoulou D, Păsăreanu CS (2003) Learning assumptions for compositional verification. In: Garavel H, Hatcliff J (eds) Proceedings of the 9th international conference on tools and algorithms for the construction and analysis of systems (TACAS ’03), Warsaw, Poland, April 7–11, 2003. Lecture notes in computer science, vol 2619. Springer, New York, pp 331–346
[13] Ernst MD, Cockrell J, Griswold WG, Notkin D (1999) Dynamically discovering likely program invariants to support program evolution. In: Proceedings of the 21st international conference on software engineering (ICSE ’99), Los Angeles, CA, May 1999. IEEE Computer Society, Los Alamitos, pp 213–224
[14] Gheorghiu M, Giannakopoulou D, Păsăreanu CS (2007) Refining interface alphabets for compositional verification. In: Grumberg O, Huth M (eds) Proceedings of the 13th international conference on tools and algorithms for the construction and analysis of systems (TACAS ’07), Braga, Portugal, March 24–April 1, 2007. Lecture notes in computer science, vol 4424. Springer, New York, pp 292–307
[15] Giannakopoulou D, Păsăreanu CS, Barringer H (2002) Assumption generation for software component verification. In: Proceedings of the 17th international conference on automated software engineering (ASE ’02), Edinburgh, Scotland, September 23–27, 2002. IEEE Computer Society, Los Alamitos, pp 3–12
[16] Groce A, Peled D, Yannakakis M (2002) Adaptive model checking. In: Katoen J-P, Stevens P (eds) Proceedings of the eighth international conference on tools and algorithms for the construction and analysis of systems (TACAS ’02), Grenoble, France, April 8–12, 2002. Lecture notes in computer science, vol 2280. Springer, New York, pp 357–370 · Zbl 1043.68570
[17] Habermehl P, Vojnar T (2005) Regular model checking using inference of regular languages. In: Proceedings of the 6th international workshop on verification of infinite-state systems (INFINITY ’04). Electronic notes in theoretical computer science, vol 138(3), pp 21–36 · Zbl 1272.68256
[18] Johnson D (1974) Approximation algorithms for combinatorial problems. J Comput Syst Sci 9(3):256–278 · Zbl 0296.65036 · doi:10.1016/S0022-0000(74)80044-9
[19] Jones CB (1983) Specification and design of (parallel) programs. In: Mason REA (ed) Proceedings of the 9th IFIP world congress. Information Processing, vol 83, Paris, France, September 1983, pp 321–332
[20] Kurshan RP (1994) Computer-aided verification of coordinating processes: the automata-theoretic approach. Princeton University Press, Princeton
[21] Misra J, Chandy KM (1981) Proofs of networks of processes. IEEE Trans Soft Eng 7(4):417–426 · Zbl 05341575 · doi:10.1109/TSE.1981.230844
[22] Peled D, Vardi MY, Yannakakis M (1999) Black box checking. In: Wu J, Chanson ST, Gao Q (eds) Proceedings of the joint international conference on formal description techniques for distributed systems and communication protocols (FORTE ’99), Beijing, China, October 1999. IFIP conference proceedings, vol 156. Kluwer Academic, Dordrecht, pp 225–240 · Zbl 0952.68012
[23] Pnueli A (1985) In transition from global to modular temporal reasoning about programs. Logics Models Concurr Syst 13:123–144 · Zbl 0578.68014
[24] Rivest RL, Schapire RE (1993) Inference of finite automata using homing sequences. Inf Comput 103(2):299–347 · Zbl 0786.68082 · doi:10.1006/inco.1993.1021
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.