article

Free access

Verification of liveness properties using compositional reachability analysis

Authors:

Shing Chi Cheung,

Dimitra Giannakopoulou,

Jeff KramerAuthors Info & Claims

ACM SIGSOFT Software Engineering Notes, Volume 22, Issue 6

Pages 227 - 243

https://doi.org/10.1145/267896.267913

Published: 01 November 1997 Publication History

PDF eReader

References

[1]

S. Aggarwal, C. Courcoubetis, and P. Wolper, "Adding Liveness Propertics to Coupled Finite-State Machines," ACM Transactions on Programming Languages and Systems, vol. 12, no. 2, 1990.

Digital Library

Google Scholar

[2]

A. V. Aho, J. E. Hopcroft, and J. D. Ullman, Data Structures and Algorithms: Addison- Wesley, 1983.

Digital Library

Google Scholar

[3]

B. Alpem and F. B. Schneider, "Verifying Temporal Properties without Temporal Logic," ACM Transactions on Programming Languages and Systems, vol. 11, no. I, pp. 147-167, 1989.

Digital Library

Google Scholar

[4]

G. R. Andrews, Concurrent Programming - Principles and Practice: The Benjamin / Cummings Publishing Company Ltd., 1991.

Digital Library

Google Scholar

[5]

G. S. Avrunin, U. A. Buy, J. C. Corbett. L. K. Dillon, and J. C. Wileden, "Automntcd Analysis of Concurrent Systems with the Constrained Expression Toolset,"IEEE Transactions on Software Engineering, vol. 17, no. 11. pp. 1204-1222, 1991.

Digital Library

Google Scholar

[6]

T. Bultan, J. Fischer, and R. Gerber, "Compositional Verification by Model Checking for Counter-Examples," presented at International Symposium on Software Testing nnd Analysis, San Diego, California, January 1996.

Digital Library

Google Scholar

[7]

S. C. Cheung and J. Kramer, "Checking,Subsystem Safety Properties in Compositibnal Reachability Analysis," presented at 18th International Conference on Softwnrc Engineering, Berlin, Germany, March 1996.

Digital Library

Google Scholar

[8]

S. C. Cheung and J. Kramer, "Context Constraints for Compositional Rcachnbility Analysis," ACM Transactions on sofhvare Engineering and Methodology, October 1996.

Digital Library

Google Scholar

[9]

E. M. Clarke, D. E. Long. and K. L. McMillan, "Compositional Model Checking," presented at 4th Annual Symposium on Logic in Computer Science, Pacific Grove, California, June 1989.

Digital Library

Google Scholar

[10]

H.-C. Femandez, L. Mounier, C. Jard, and T. Jeron, "On-the-fly Verification of Finite Transition Systems," in Computer-Aided Verification, R. Kurshan, Ed.: Kluwer Academic Publishers, 1993.

Google Scholar

[11]

C, Ghezzi, M. Jazayeri. and D. Mandrioli, Fundamentals of Software Engineering, Chapter 6: Prentice-Hall, Inc., 1991.

Digital Library

Google Scholar

[12]

D. Giannakopoulou, J. Kramer, and S. C. Cheung, "TRACTAz An Environment for Analysing the Behaviour of Distributed Systems," presented at ACM SIGPLAN Workshop on Automated Analysis of Software, Paris, January 1997.

Google Scholar

[13]

P. Godefroid and G. J. Holzmann. "On the Verification of Temporal Properties," presented at 13th IFlP WG 6.1 International Symposium, on Protocol Specification, Testing, and Verification.

Digital Library

Google Scholar

[14]

P. Gribomont and P. Wolper, "Temporal Logic," in From Modal Logic to Deductive Databases, A. Thayse, Ed.: John Wiley and Sons, 1989.

Google Scholar

[15]

C. A. R, Hoare, Communicating Sequential Processes: Prentice-Hall, 1985.

Digital Library

Google Scholar

[16]

J. Kemppainen, M. Levanto, A. Valmari, and M. Clegg, ARA Puts Advanced Reachability Analysis Techniques Together," presented at 5th Nordic Workshop on Programming Environment Research, Tampere, Finland, January 1992.

Google Scholar

[17]

J. Kramer and J. Magee, "Exposing the Skeleton in the Coordination Closet," presented at Coordination '97, Berlin, September 1997.

Digital Library

Google Scholar

[18]

J. C. Lin and S. Paul, "RMTP: A Reliable Multicast Transport Protocol," presented at IEEE INFOCOMM'96, San Francisco, California, March 1996.

Digital Library

Google Scholar

[19]

J. Malhotra, S. A. Smolka, A. Giacalone, and R. Shapiro, "A Tool for Hierarchical Design and Simulation of Concurrent Systems" presented at BCS-FACS Workshop on Specification and Verification of Concurrent Systems, Stirling, Scotland, July 1988.

Digital Library

Google Scholar

[20]

R. Milner, Communication and Concurrency: Prentice-Hall, 1989.

Digital Library

Google Scholar

[21]

A. Rabinovich, "Checking Equivalences Between Concurrent Systems of Finite Agents," presented at 19th International Colloquium on Automata, Languages and Programming, Wien, Austria, July 1992.

Digital Library

Google Scholar

[22]

K. K. Sabnani, A. M. Lapone, and M. U. Uyar, "An Algorithmic Procedure for Checking Safety Properties of Protocols," IEEE Transactions on Communications, vol. 37, no. 9, pp. 940-948, September 1989.

Google Scholar

[23]

K. C. Tai and P. V. Koppol, "Hierarchy-Based Incremental Reachability Analysis of Communication Protocols," presented at IEEE International Conference on Network Protocols, San Francisco, California, October 1993.

Google Scholar

[24]

A. Valmari. Alleviating State Explosion during Verification of Behavioural Equivalence, Technical Report, A-1992, Department of Computer Science, University of Helsinki, Finland, August 1992.

Google Scholar

[25]

W. J. Yeh. Controlling State Explosion in Reachability Analysis, Technical Report, SERC-TR-147-P, SERC, Purdue University, December 1993.

Digital Library

Google Scholar

[26]

W. J. Yeh and M. Young, "Compositional Reachability Analysis Using Process Algebra," presented at Symposium on Testing, Analysis, and Verification (TAV4), Victoria, British Columbia, October 8-10, 1991.

Digital Library

Google Scholar

[27]

W. J. Yeh and M. Young, "Hierarchical Tracing of Concurrent Programs,"Presented at 3rd Irvine Software Symposium (ISS93), Irvine, California, April 1993.

Google Scholar

Cited By

View all

Isazadeh AKarimpour J(2018)A new formalism for mathematical description and verification of component-based systemsThe Journal of Supercomputing10.1007/s11227-008-0240-y49:3(334-353)Online publication date: 30-Dec-2018
https://dl.acm.org/doi/10.1007/s11227-008-0240-y
Chen BLi CCai Q(2009)Composite E-services Behavioral Requirements Based on Activity Chain and Their Dynamic Operation SemanticsProceedings of the 2009 International Conference on Multimedia Information Networking and Security - Volume 0110.1109/MINES.2009.173(595-598)Online publication date: 18-Nov-2009
https://dl.acm.org/doi/10.1109/MINES.2009.173
Jiang JShi M(2004)CoAuto: A Formal Model for Cooperative ProcessesGrid and Cooperative Computing10.1007/978-3-540-24680-0_105(660-668)Online publication date: 2004
https://doi.org/10.1007/978-3-540-24680-0_105
Show More Cited By

Index Terms

Verification of liveness properties using compositional reachability analysis

Recommendations

Verification of liveness properties using compositional reachability analysis
ESEC '97/FSE-5: Proceedings of the 6th European SOFTWARE ENGINEERING conference held jointly with the 5th ACM SIGSOFT international symposium on Foundations of software engineering
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 ...
Compositional verification of concurrent systems using Petri-net-based condensation rules

The state-explosion problem of formal verification has obstructed its application to large-scale software systems. In this article, we introduce a set of new condensation theories: IOT-failure equivalence, IOT-state equivalence, and firing-dependence ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM SIGSOFT Software Engineering Notes

ACM SIGSOFT Software Engineering Notes Volume 22, Issue 6

Nov. 1997

527 pages

ISSN:0163-5948

DOI:10.1145/267896

Editors:
Mehdi Jazayeri
Technische Univ. Wien, Vienna, Austria
,
Helmut Schauer
Univ. of Zurich, Zurich, Switzerland

Issue’s Table of Contents

ESEC '97/FSE-5: Proceedings of the 6th European SOFTWARE ENGINEERING conference held jointly with the 5th ACM SIGSOFT international symposium on Foundations of software engineering
November 1997
536 pages
ISBN:3540635319
Editors:
Mehdi Jazayeri
Technische Univ. Wien, Vienna, Austria
,
Helmut Schauer
Univ. Zurich, Zurich, Switzerland

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 November 1997

Published in SIGSOFT Volume 22, Issue 6

Check for updates

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

17
Total Citations
View Citations
521
Total Downloads

Downloads (Last 12 months)89
Downloads (Last 6 weeks)13

Reflects downloads up to 30 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Isazadeh AKarimpour J(2018)A new formalism for mathematical description and verification of component-based systemsThe Journal of Supercomputing10.1007/s11227-008-0240-y49:3(334-353)Online publication date: 30-Dec-2018
https://dl.acm.org/doi/10.1007/s11227-008-0240-y
Chen BLi CCai Q(2009)Composite E-services Behavioral Requirements Based on Activity Chain and Their Dynamic Operation SemanticsProceedings of the 2009 International Conference on Multimedia Information Networking and Security - Volume 0110.1109/MINES.2009.173(595-598)Online publication date: 18-Nov-2009
https://dl.acm.org/doi/10.1109/MINES.2009.173
Jiang JShi M(2004)CoAuto: A Formal Model for Cooperative ProcessesGrid and Cooperative Computing10.1007/978-3-540-24680-0_105(660-668)Online publication date: 2004
https://doi.org/10.1007/978-3-540-24680-0_105
Kramer JMagee J(1998)Analysing dynamic change in software architectures: a case studyProceedings. Fourth International Conference on Configurable Distributed Systems (Cat. No.98EX159)10.1109/CDS.1998.675762(91-100)Online publication date: 1998
https://doi.org/10.1109/CDS.1998.675762
Attie PLorenz DPortnova AChockler H(2006)Behavioral compatibility without state explosionProceedings of the 9th international conference on Component-Based Software Engineering10.1007/11783565_3(33-49)Online publication date: 29-Jun-2006
https://dl.acm.org/doi/10.1007/11783565_3
Clarke LChen YAvrunin GChen BCobleigh RFrederick KHenneman EOsterweil L(2005)Process programming to support medical safetyProceedings of the 2005 international conference on Unifying the Software Process Spectrum10.1007/11608035_29(347-359)Online publication date: 25-May-2005
https://dl.acm.org/doi/10.1007/11608035_29
Cheng Y(2005)Crafting a promela front-end with abstract data types to mitigate the sensitivity of (compositional) analysis to implementation choicesProceedings of the 12th international conference on Model Checking Software10.1007/11537328_13(139-153)Online publication date: 22-Aug-2005
https://dl.acm.org/doi/10.1007/11537328_13
Xie FBrowne J(2003)Verified systems by composition from verified componentsACM SIGSOFT Software Engineering Notes10.1145/949952.94010928:5(277-286)Online publication date: 1-Sep-2003
https://dl.acm.org/doi/10.1145/949952.940109
Xie FBrowne JPaakki JInverardi P(2003)Verified systems by composition from verified componentsProceedings of the 9th European software engineering conference held jointly with 11th ACM SIGSOFT international symposium on Foundations of software engineering10.1145/940071.940109(277-286)Online publication date: 1-Sep-2003
https://dl.acm.org/doi/10.1145/940071.940109
Barber KGraser THolt JBaker G(2003)ArcadeRequirements Engineering10.1007/s00766-002-0159-48:4(222-235)Online publication date: 1-Nov-2003
https://dl.acm.org/doi/10.1007/s00766-002-0159-4
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Login options

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

References

Cited By

Index Terms

Recommendations