article

Automatic symbolic compositional verification by learning assumptions

Authors:

Rajeev AlurAuthors Info & Claims

Formal Methods in System Design, Volume 32, Issue 3

Pages 207 - 234

https://doi.org/10.1007/s10703-008-0055-8

Published: 01 June 2008 Publication History

Abstract

Compositional reasoning aims to improve scalability of verification tools by reducing the original verification task into subproblems. The simplification is typically based on assume-guarantee reasoning principles, and requires user guidance to identify appropriate assumptions for components. In this paper, we propose a fully automated approach to compositional reasoning that consists of automated decomposition using a hypergraph partitioning algorithm for balanced clustering of variables, and discovering assumptions using the L ^* algorithm for active learning of regular languages. We present a symbolic implementation of the learning algorithm, and incorporate it in the model checker NuSmv . In some cases, our experiments demonstrate significant savings in the computational requirements of symbolic model checking.

References

[1]

Abadi M, Lamport L (1995) Conjoining specifications. ACM Trans Program Lang Syst (TOPLAS) 17:507-534.

Digital Library

[2]

Alur R, Henzinger T (1999) Reactive modules. Form Methods Syst Des 15(1):7-48. Invited submission to FLoC'96 special issue. A preliminary version appears in Proceedings of the 11th LICS, 1996 .

Digital Library

[3]

Alur R, Henzinger T, Mang F, Qadeer S, Rajamani S, Tasiran S (1998) MOCHA: Modularity in model checking. In: Proceedings of the 10th international conference on computer aided verification, pp 516- 520.

[4]

Alur R, de Alfaro L, Henzinger T, Mang F (1999) Automating modular verification. In: CONCUR'99: Concurrency theory, tenth international conference. LNCS, vol 1664. Springer, Berlin, pp 82-97.

[5]

Alur R, Cerny P, Madhusudan P, Nam W (2005) Synthesis of interface specifications for Java classes. In: Proceedings of the 32nd symposium on principles of programming languages, POPL 2005, pp 98-109.

[6]

Alur R, Madhusudan P, Nam W (2005) Symbolic compositional verification by learning assumptions. In: Proceedings of the 17th international conference of computer aided verification, CAV 2005, pp 548-562.

[7]

Angluin D, (1987) Learning regular sets from queries and counterexamples. Inf Comput 75:87-106.

Digital Library

[8]

Barringer H, Pasareanu C, Giannakopoulou D (2003) Proof rules for automated compositional verification through learning. In: Proceedings of the 2nd international workshop on specification and verification of component based systems.

[9]

Biere A, Cimatti A, Clarke E, Zhu Y (1999) Symbolic model checking without BDDs. In: Proceedings of the 5th international conference on tools and algorithms for the construction and analysis of systems, pp 193-207.

[10]

Birkendorf A, Böker A, Simon H-U (2000) Learning deterministic finite automata from smallest counter examples. SIAM J Discrete Math 13(4):465-491.

Digital Library

[11]

Bryant R, (1986) Graph-based algorithms for boolean-function manipulation. IEEE Trans Comput, C-35(8).

[12]

Cimatti A, Clarke E, Giunchiglia E, Giunchiglia F, Pistore M, Roveri M, Sebastiani R, Tacchella A (2002) NuSMV Version 2: An OpenSource tool for symbolic model checking. In: Proceedings of the 14th international conference on computer-aided verification (CAV 2002). LNCS, vol 2404. Springer, Berlin, pp 359-364.

[13]

Clarke E, Grumberg O, Jha S, Lu Y, Veith H (2000) Counterexample-guided abstraction refinement. In: Proceedings of international conference on computer aided verification (CAV'00), pp 154-169.

[14]

Cobleigh J, Giannakopoulou D, Pasareanu C (2003) Learning assumptions for compositional verification. In: Proceedings of the 9th international conference on tools and algorithms for the construction and analysis of software. LNCS, vol 2619. Springer, Berlin, pp 331-346.

[15]

Cobleigh J, Avrunin G, Clarke L. (2006) Breaking up is hard to do: An investigation of decomposition for assume-guarantee reasoning. In: Proceedings of the international symposium on software testing and analysis, pp 97-108.

[16]

Fiduccia C, Mattheyses R (1982) A linear-time heuristic for improving network partitions. In: proceedings of the 19th design automation conference, pp 241-247.

[17]

Giannakopoulou D, Pasareanu C, (2005) Learning-based assume-guarantee verification, In: Proceeding of the 12th international spin workshop, pp 282-287.

[18]

Giannakopoulou D, Pasareanu C, Barringer H (2002) Assumption generation for software component verification. In: Proceedings of 17th IEEE international conference on automated software engineering (ASE 2002), pp 3-12.

[19]

Grümberg O, Long D (1994) Model checking and modular verification. ACM Trans Program Lang Syst 16(3):843-871.

Digital Library

[20]

Gupta A, McMillan K, Fu Z (2007) Automated assumption generation for compositional verification. In: Proceedings of the 19th international conference of computer aided verification, CAV 2007, pp 420-432.

[21]

Henzinger T, Qadeer S, Rajamani S (1998) You assume, we guarantee: Methodology and case studies. In: CAV 98: Computer-aided verification. LNCS, vol 1427. Springer, Berlin, pp 521-525.

[22]

Ibarra O, Jiang T (1991) Learning regular languages from counterexamples. J Comput Syst Sci 43(2):299-316.

Digital Library

[23]

Jones C (1981) Development methods for computer programs including a notion of interference. PhD thesis, Oxford University.

[24]

Karypis G, Kumar V (1999) Multilevel k -way hypergraph partitioning. In: Proceedings of the 36th conference on design automation, pp 343-348.

[25]

Karypis G, Aggarwal R, Kumar V, Shekhar S (1999) Multilevel hypergraph partitioning: applications in VLSI domain. IEEE Trans Very Large Scale Integr (VLSI) Syst 7(1):69-79.

Digital Library

[26]

Kearns M, Vazirani U (1994) An introduction to computational learning theory. MIT Press, Cambridge.

[27]

Kernighan B, Lin S (1970) An efficient heuristic procedure for partitioning graphs. Bell Syst Tech J 49(2):291-307.

[28]

Kurshan R (1994) Computer-aided Verification of Coordinating Processes: The automata-theoretic approach. Princeton University Press, Princeton.

[29]

McMillan K (1997) A compositional rule for hardware design refinement. In: Proceedings of the 9th international conference on computer aided verification, pp 24-35.

[30]

McMillan K (2002) Applying SAT methods in unbounded symbolic model checking. In: Proceedings of the 14th international conference on computer aided verification. LNCS, vol 2404. Springer, Berlin, pp 250-264.

[31]

Misra J, Chandy K (198l) Proofs of networks of processes. IEEE Trans Softw Eng 7(4):417-426.

[32]

Nam W, Alur R (2006) Learning-based symbolic assume-guarantee reasoning with automatic decomposition. In: Proceedings of the 4th international symposium on automated technology for verification and analysis (ATVA'06), pp 170-185.

[33]

Nam W, Alur R (2007) Learning plans for safety and reachability goals with partial observability. Technical Report MS-CIS-07-16, University of Pennsylvania.

[34]

Namjoshi K, Trefler R (2000) On the completeness of compositional reasoning. In: Proceedings of the 12th international conference of computer aided verification, CAV 2000, pp 139-153.

[35]

Peled D, Vardi M, Yannakakis M (2002) Black box checking. J Aurora Lang Comb 7(2):225-246.

[36]

Pnueli A (1984) In transition from global to modular temporal reasoning about programs. In: Logics and Models of Concurrent Systems. Springer, New York, pp 123-144.

[37]

Rivest R, Schapire R (1993) Inference of finite automata using homing sequences, Inf Comput 103(2):299-347.

Digital Library

[38]

Sharygina N, Chaki S, Clarke E, Sinha N (2005) Dynamic component substitutability analysis. In: Proceedings of the international symposium of formal methods Europe, pp 512-528.

[39]

Sinha N, Clarke E (2007) SAT-based compositional verification using lazy learning. In: Proceedings of the 19th international conference of computer aided verification, CAV 2007, pp 39-54.

[40]

Stark E (1985) A proof technique for rely-guarantee properties. In: FST & TCS 85: Foundations of software technology and theoretical computer science. LNCS, vol 206. Springer, Berlin, pp 369-391.

[41]

Vardhan A, Viswanathan M (2006) Lever: A tool for learning based verification. In: Proceedings of 18th international conference on computer aided verification (CAV 2006), pp 471-474.

[42]

Vardhan A, Sen K, Viswanathan M, Agha G (2004) Actively learning to verify safety properties for FIFO automata. In: Proceedings of 24th foundations of software technology and theoretical computer science. LNCS, vol 3328. Springer, Berlin, pp 494-505.

Cited By

Abbasi RGhassemi FKhosravi R(2019)Verification of asynchronous systems with an unspecified componentActa Informatica10.1007/s00236-018-0317-x56:2(161-203)Online publication date: 1-Mar-2019
https://dl.acm.org/doi/10.1007/s00236-018-0317-x
Meller YGrumberg OShoham S(2016)A framework for compositional verification of multi-valued systems via abstraction-refinementInformation and Computation10.1016/j.ic.2016.01.001247:C(169-202)Online publication date: 1-Apr-2016
https://dl.acm.org/doi/10.1016/j.ic.2016.01.001
Choi YPark MByun TKim D(2015)Efficient safety checking for automotive operating systems using property-based slicing and constraint-based environment generationScience of Computer Programming10.1016/j.scico.2014.10.006103:C(51-70)Online publication date: 1-Jun-2015
https://dl.acm.org/doi/10.1016/j.scico.2014.10.006
Show More Cited By

Index Terms

Automatic symbolic compositional verification by learning assumptions

Recommendations

Symbolic assume-guarantee reasoning through BDD learning
ICSE 2014: Proceedings of the 36th International Conference on Software Engineering

Both symbolic model checking and assume-guarantee reasoning aim to circumvent the state explosion problem. Symbolic model checking explores many states simultaneously and reports numerous erroneous traces. Automated assume-guarantee reasoning, on the ...
Compositional reachability analysis for efficient modular verification of asynchronous designs

Compositional verification is essential to address state explosion in model checking. Traditionally, an over-approximate context is needed for each individual component in a system for sound verification. This may cause state explosion for the ...
Learning-based symbolic assume-guarantee reasoning for Markov decision process by using interval Markov process

Many real-life critical systems are described with large models and exhibit both probabilistic and non-deterministic behaviour. Verification of such systems requires techniques to avoid the state space explosion problem. Symbolic model checking and ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Formal Methods in System Design

Formal Methods in System Design Volume 32, Issue 3

June 2008

128 pages

ISSN:0925-9856

Issue’s Table of Contents

Copyright © Copyright © 2008 Springer Science+Business Media, LLC.

Publisher

Kluwer Academic Publishers

United States

Publication History

Published: 01 June 2008

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

12
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 14 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Abbasi RGhassemi FKhosravi R(2019)Verification of asynchronous systems with an unspecified componentActa Informatica10.1007/s00236-018-0317-x56:2(161-203)Online publication date: 1-Mar-2019
https://dl.acm.org/doi/10.1007/s00236-018-0317-x
Meller YGrumberg OShoham S(2016)A framework for compositional verification of multi-valued systems via abstraction-refinementInformation and Computation10.1016/j.ic.2016.01.001247:C(169-202)Online publication date: 1-Apr-2016
https://dl.acm.org/doi/10.1016/j.ic.2016.01.001
Choi YPark MByun TKim D(2015)Efficient safety checking for automotive operating systems using property-based slicing and constraint-based environment generationScience of Computer Programming10.1016/j.scico.2014.10.006103:C(51-70)Online publication date: 1-Jun-2015
https://dl.acm.org/doi/10.1016/j.scico.2014.10.006
Meller YGrumberg OYorav K(2015)Learning-Based Compositional Model Checking of Behavioral UML SystemsRevised Selected Papers of the 12th International Conference on Formal Aspects of Component Software - Volume 953910.1007/978-3-319-28934-2_15(275-293)Online publication date: 14-Oct-2015
https://dl.acm.org/doi/10.1007/978-3-319-28934-2_15
He FWang BYin LZhu LJalote PBriand LHoek A(2014)Symbolic assume-guarantee reasoning through BDD learningProceedings of the 36th International Conference on Software Engineering10.1145/2568225.2568253(1071-1082)Online publication date: 31-May-2014
https://dl.acm.org/doi/10.1145/2568225.2568253
Feng LKwiatkowska MParker D(2011)Automated learning of probabilistic assumptions for compositional reasoningProceedings of the 14th international conference on Fundamental approaches to software engineering: part of the joint European conferences on theory and practice of software10.5555/1987434.1987437(2-17)Online publication date: 26-Mar-2011
https://dl.acm.org/doi/10.5555/1987434.1987437
Nguyen TSun JLiu YDong J(2011)A model checking framework for hierarchical systemsProceedings of the 26th IEEE/ACM International Conference on Automated Software Engineering10.1109/ASE.2011.6100143(633-636)Online publication date: 6-Nov-2011
https://dl.acm.org/doi/10.1109/ASE.2011.6100143
Lomuscio AStrulo BWalker NWu P(2010)Assume-guarantee reasoning with local specificationsProceedings of the 12th international conference on Formal engineering methods and software engineering10.5555/1939864.1939883(204-219)Online publication date: 17-Nov-2010
https://dl.acm.org/doi/10.5555/1939864.1939883
Chen YClarke EFarzan AHe FTsai MTsay YWang BZhu L(2010)Comparing learning algorithms in automated assume-guarantee reasoningProceedings of the 4th international conference on Leveraging applications of formal methods, verification, and validation - Volume Part I10.5555/1939281.1939341(643-657)Online publication date: 18-Oct-2010
https://dl.acm.org/doi/10.5555/1939281.1939341
Nam WAlur R(2010)Active learning of plans for safety and reachability goals with partial observabilityIEEE Transactions on Systems, Man, and Cybernetics, Part B: Cybernetics10.1109/TSMCB.2009.202565740:2(412-420)Online publication date: 1-Apr-2010
https://dl.acm.org/doi/10.1109/TSMCB.2009.2025657
Show More Cited By

View Options

View options

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Issue’s Table of Contents