More Web Proxy on the site http://driver.im/

Article

Learning assumptions for compositional verification

Authors:

Jamieson M. Cobleigh,

Dimitra Giannakopoulou,

Corina S. PăsăreanuAuthors Info & Claims

TACAS'03: Proceedings of the 9th international conference on Tools and algorithms for the construction and analysis of systems

Pages 331 - 346

Published: 07 April 2003 Publication History

Abstract

Compositional verification is a promising approach to addressing the state explosion problem associated with model checking. One compositional technique advocates proving properties of a system by checking properties of its components in an assume-guarantee style. However, the application of this technique is difficult because it involves non-trivial human input. This paper presents a novel framework for performing assume-guarantee reasoning in an incremental and fully automated fashion. To check a component against a property, our approach generates assumptions that the environment needs to satisfy for the property to hold. These assumptions are then discharged on the rest of the system. Assumptions are computed by a learning algorithm. They are initially approximate, but become gradually more precise by means of counterexamples obtained by model checking the component and its environment, alternately. This iterative process may at any stage conclude that the property is either true or false in the system. We have implemented our approach in the LTSA tool and applied it to a NASA system.

References

[1]

R. Alur, T. A. Henzinger, and O. Kupferman. Alternating-time temporal logic. In Compositionality: The Significant Difference - An International Symposium, 1997.

Digital Library

[2]

R. Alur, T. A. Henzinger, F. Y. C. Mang, S. Qadeer, S. K. Rajamani, and S. Tasiran. MOCHA: Modularity in model checking. In Proc. of the 10th Int. Conf. on Computer-Aided Verification, pages 521-525, June 28-July 2, 1998.

Digital Library

[3]

D. Angluin. Learning regular sets from queries and counterexamples. Information and Computation, 75(2):87-106, Nov. 1987.

Digital Library

[4]

S. C. Cheung and J. Kramer. Context constraints for compositional reachability analysis. ACM Transactions on Software Engineering and Methodology, 5(4):334- 377, Oct. 1996.

Digital Library

[5]

S. C. Cheung and J. Kramer. Checking safety properties using compositional reachability analysis. ACM Transactions on Software Engineering and Methodology , 8(1):49-78, Jan. 1999.

Digital Library

[6]

T. S. Chow. Testing software design modeled by finite-state machines. IEEE Transactions on Software Engineering, SE-4(3):178-187, May 1978.

Digital Library

[7]

E. M. Clarke, D. E. Long, and K. L. McMillan. Compositional model checking. In Proc. of the 4th Symp. on Logic in Computer Science, pages 353-362, June 1989.

Digital Library

[8]

E. M. Clarke, O. Grumberg, and D. A. Peled. Model Checking. MIT Press, 1999.

Digital Library

[9]

L. de Alfaro and T. A. Henzinger. Interface automata. In Proc. of the 8th European Software Engineering Conf. held jointly with the 9th ACM SIGSOFT Symp. on the Foundations of Software Engineering, pages 109-120, Sept. 2001.

Digital Library

[10]

L. de Alfaro and T. A. Henzinger. Interface theories for component-based design. In Proc. of the 1st Int. Workshop on Embedded Software, pages 148-165, Oct. 2001.

Digital Library

[11]

T. Dean and M. S. Boddy. An analysis of time-dependent planning. In Proc. of the 7th National Conf. on Artificial Intelligence, pages 49-54, Aug. 1988.

[12]

C. Flanagan, S. N. Freund, and S. Qadeer. Thread-modular verification for shared-memory programs. In Proc. of the 11th European Symp. on Programming, pages 262-277, Apr. 2002.

Digital Library

[13]

D. Giannakopoulou, J. Kramer, and S. C. Cheung. Behaviour analysis of distributed systems using the Tracta approach. Automated Software Engineering, 6(1):7-35, July 1999.

Digital Library

[14]

D. Giannakopoulou, C. S. Pasareanu, and H. Barringer. Assumption generation for software component verification. In Proc. of the 17th IEEE Int. Conf. on Automated Software Engineering, Sept. 2002.

Digital Library

[15]

A. Groce, D. Peled, and M. Yannakakis. Adaptive model checking. In Proc. of the 8th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems, pages 357-370, Apr. 2002.

Digital Library

[16]

O. Grumberg and D. E. Long. Model checking and modular verification. In Proc. of the 2nd Int. Conf. on Concurrency Theory, pages 250-265, Aug. 1991.

Digital Library

[17]

T. A. Henzinger, S. Qadeer, and S. K. Rajamani. You assume, we guarantee: Methodology and case studies. In Proc. of the 10th Int. Conf. on Computer-Aided Verification, pages 440-451, June 28-July 2, 1998.

Digital Library

[18]

C. B. Jones. Specification and design of (parallel) programs. In R. Mason, editor, Information Processing 83: Proc. of the IFIP 9th World Congress, pages 321-332. IFIP: North Holland, 1983.

[19]

J.-P. Krimm and L. Mounier. Compositional state space generation from Lotos programs. In Proc. of the 3rd Int. Workshop on Tools and Algorithms for the Construction and Analysis of Systems, pages 239-258, Apr. 1997.

Digital Library

[20]

J. Magee and J. Kramer. Concurrency: State Models & Java Programs. John Wiley & Sons, 1999.

Digital Library

[21]

A. Pnueli. In transition from global to modular temporal reasoning about programs. In K. Apt, editor, Logic and Models of Concurrent Systems, volume 13, pages 123-144, New York, 1984. Springer-Verlag.

Digital Library

[22]

R. L. Rivest and R. E. Schapire. Inference of finite automata using homing sequences. Information and Computation, 103(2):299-347, Apr. 1993.

Digital Library

[23]

W. Visser, K. Havelund, G. Brat, and S.-J. Park. Model checking programs. In Proc. of the 15th IEEE Int. Conf. on Automated Software Engineering, Sept. 2000.

Digital Library

[24]

Q. Xu, W. P. de Roever, and J. He. The rely-guarantee method for verifying shared variable concurrent programs. Formal Aspects of Computing, 9(2):149-174, 1997.

Cited By

Kang EGalster MMirakhorli MWilliams L(2020)Robustness analysis for secure software designProceedings of the 3rd ACM SIGSOFT International Workshop on Software Security from Design to Deployment10.1145/3416507.3423191(19-25)Online publication date: 9-Nov-2020
https://dl.acm.org/doi/10.1145/3416507.3423191
Gaaloul KMenghi CNejati SBriand LWolfe DDevanbu PCohen MZimmermann T(2020)Mining assumptions for software components using machine learningProceedings of the 28th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering10.1145/3368089.3409737(159-171)Online publication date: 8-Nov-2020
https://dl.acm.org/doi/10.1145/3368089.3409737
Tran HNguyen QHung P(2019)On Implementation of the Improved Assume-Guarantee Verification Method for Timed SystemsProceedings of the 10th International Symposium on Information and Communication Technology10.1145/3368926.3369659(457-464)Online publication date: 4-Dec-2019
https://dl.acm.org/doi/10.1145/3368926.3369659
Show More Cited By

Learning assumptions for compositional verification
1. Software and its engineering
  1. Software organization and properties
    1. Software functional properties
      1. Formal methods
2. Theory of computation

Recommendations

Automatic symbolic compositional verification by learning assumptions

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 ...
Learning Assumptions for Compositional Verification of Timed Automata
Computer Aided Verification
Abstract
Compositional verification, such as the technique of assume-guarantee reasoning (AGR), is to verify a property of a system from the properties of its components. It is essential to address the state explosion problem associated with model ...
Automated interface refinement for compositional verification

Compositional verification is essential for verifying large systems. However, approximate environments are needed when verifying the constituent modules in a system. Effective compositional verification requires finding a simple but accurate ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

TACAS'03: Proceedings of the 9th international conference on Tools and algorithms for the construction and analysis of systems

April 2003

603 pages

ISBN:3540008985

Editors:
Hubert Garavel
INRIA Rhôe-Alpes, Montbonnot Saint Martin, France
,
John Hatcliff
Kansas State University, Department of Computing and Information Sciences, Manhattan, KS

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 07 April 2003

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

122
Total Citations
View Citations
0
Total Downloads

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

Reflects downloads up to 12 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Kang EGalster MMirakhorli MWilliams L(2020)Robustness analysis for secure software designProceedings of the 3rd ACM SIGSOFT International Workshop on Software Security from Design to Deployment10.1145/3416507.3423191(19-25)Online publication date: 9-Nov-2020
https://dl.acm.org/doi/10.1145/3416507.3423191
Gaaloul KMenghi CNejati SBriand LWolfe DDevanbu PCohen MZimmermann T(2020)Mining assumptions for software components using machine learningProceedings of the 28th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering10.1145/3368089.3409737(159-171)Online publication date: 8-Nov-2020
https://dl.acm.org/doi/10.1145/3368089.3409737
Tran HNguyen QHung P(2019)On Implementation of the Improved Assume-Guarantee Verification Method for Timed SystemsProceedings of the 10th International Symposium on Information and Communication Technology10.1145/3368926.3369659(457-464)Online publication date: 4-Dec-2019
https://dl.acm.org/doi/10.1145/3368926.3369659
Berglund LArtho C(2019)Method summaries for JPFACM SIGSOFT Software Engineering Notes10.1145/3364452.3364456044:4(16-16)Online publication date: 12-Dec-2019
https://dl.acm.org/doi/10.1145/3364452.33644560
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
Íncer Romeo ÍSangiovanni-Vincentelli ALin CKang EHu KZhan N(2018)Quotient for assume-guarantee contractsProceedings of the 16th ACM-IEEE International Conference on Formal Methods and Models for System Design10.5555/3343872.3343881(67-77)Online publication date: 15-Oct-2018
https://dl.acm.org/doi/10.5555/3343872.3343881
Bouchekir RBoukala M(2018)Learning-based symbolic assume-guarantee reasoning for Markov decision process by using interval Markov processInnovations in Systems and Software Engineering10.1007/s11334-018-0316-714:3(229-244)Online publication date: 1-Sep-2018
https://dl.acm.org/doi/10.1007/s11334-018-0316-7
Dillig IDillig TLi BMcmillan KSagiv M(2017)Synthesis of circular compositional program proofs via abductionInternational Journal on Software Tools for Technology Transfer (STTT)10.1007/s10009-015-0397-719:5(535-547)Online publication date: 1-Oct-2017
https://dl.acm.org/doi/10.1007/s10009-015-0397-7
Bak SChaki S(2016)Verifying cyber-physical systems by combining software model checking with hybrid systems reachabilityProceedings of the 13th International Conference on Embedded Software10.1145/2968478.2968490(1-10)Online publication date: 1-Oct-2016
https://dl.acm.org/doi/10.1145/2968478.2968490
Garg PNeider DMadhusudan PRoth D(2016)Learning invariants using decision trees and implication counterexamplesACM SIGPLAN Notices10.1145/2914770.283766451:1(499-512)Online publication date: 11-Jan-2016
https://dl.acm.org/doi/10.1145/2914770.2837664
Show More Cited By

View Options

View options

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 Table of Contents