Verification of liveness properties using compositional reachability analysis

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Verification of liveness properties using compositional reachability analysis

Full text

Pdf (1.38 MB)

Source

Foundations of Software Engineering archive
Proceedings of the 6th European SOFTWARE ENGINEERING conference held jointly with the 5th ACM SIGSOFT international symposium on Foundations of software engineering table of contents

Zurich, Switzerland

Pages: 227 - 243

Year of Publication: 1997

ISBN:3-540-63531-9

Also published in ...

Authors

Shing Chi Cheung	Department of Computer Science, Hong Kong University of Science and Technology, Clear Water Bay, Hong Kong
Dimitra Giannakopoulou	Department of Computing, Imperial College of Science, Technology and Medicine, London SW7 2B2, UK
Jeff Kramer	Department of Computing, Imperial College of Science, Technology and Medicine, London SW7 2B2, UK

Sponsors

University of Zurich : University of Zurich
CEPIS : Council of European Professional Informatics Societies
SIGSOFT: ACM Special Interest Group on Software Engineering
Swiss Informaticians Society : Swiss Information Society

Publisher

Springer-Verlag New York, Inc. New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 2, Downloads (12 Months): 30, Citation Count: 10

Additional Information:

references cited by index terms collaborative colleagues

Tools and Actions:	Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/267895.267913 What is a DOI?

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	S. Aggarwal , C. Courcoubetis , P. Wolper, Adding liveness properties to coupled finite-state machines, ACM Transactions on Programming Languages and Systems (TOPLAS), v.12 n.2, p.303-339, April 1990 [doi>10.1145/78942.78948]
	2	Alfred V. Aho , John E. Hopcroft , Jeffrey Ullman , J. D. Ullman , J. E. Hopcroft, Data Structures and Algorithms, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1983
	3	Bowen Alpern , Fred B. Schneider, Verifying temporal properties without temporal logic, ACM Transactions on Programming Languages and Systems (TOPLAS), v.11 n.1, p.147-167, Jan. 1989 [doi>10.1145/59287.62028]
	4	Gregory R. Andrews, Concurrent programming: principles and practice, Benjamin-Cummings Publishing Co., Inc., Redwood City, CA, 1991
	5	George S. Avrunin , Ugo A. Buy , James C. Corbett , Laura K. Dillon , Jack C. Wileden, Automated Analysis of Concurrent Systems with the Constrained Expression Toolset, IEEE Transactions on Software Engineering, v.17 n.11, p.1204-1222, November 1991 [doi>10.1109/32.106975]
	6	Tevfik Bultan , Jeffrey Fischer , Richard Gerber, Compositional verification by model checking for counter-examples, Proceedings of the 1996 ACM SIGSOFT international symposium on Software testing and analysis, p.224-238, January 08-10, 1996, San Diego, California, United States
	7	Shing C. Cheung , Jeff Kramer, Checking subsystem safety properties in compositional reachability analysis, Proceedings of the 18th international conference on Software engineering, p.144-154, March 25-29, 1996, Berlin, Germany
	8	Shing Chi Cheung , Jeff Kramer, Context constraints for compositional reachability analysis, ACM Transactions on Software Engineering and Methodology (TOSEM), v.5 n.4, p.334-377, Oct. 1996 [doi>10.1145/235321.235323]
	9	E. Clarke , D. Long , K. McMillan, Compositional model checking, Proceedings of the Fourth Annual Symposium on Logic in computer science, p.353-362, June 1989, Pacific Grove, California, United States
	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.
	11	Carlo Ghezzi , Mehdi Jazayeri , Dino Mandrioli, Fundamentals of software engineering, Prentice-Hall, Inc., Upper Saddle River, NJ, 1991
	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.
	13	Patrice Godefroid , Gerard J. Holzmann, On the Verification of Temporal Properties, Proceedings of the IFIP TC6/WG6.1 Thirteenth International Symposium on Protocol Specification, Testing and Verification XIII, p.109-124, May 25-28, 1993
	14	P. Gribomont and P. Wolper, "Temporal Logic," in From Modal Logic to Deductive Databases, A. Thayse, Ed.: John Wiley and Sons, 1989.
	15	C. A. R. Hoare, Communicating sequential processes, Prentice-Hall, Inc., Upper Saddle River, NJ, 1985
	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.
	17	Jeff Kramer , Jeff Magee, Exposing the Skeleton in the Coordination Closet, Proceedings of the Second International Conference on Coordination Languages and Models, p.18-31, September 01-03, 1997
	18	J. C. Lin and S. Paul, "RMTP: A Reliable Multicast Transport Protocol," presented at IEEE INFOCOMM'96, San Francisco, California, March 1996.
	19	Jawahar Malhotra , Robert M. Shapiro , Scott A. Smolka , Alessandro Giacalone, Winston: A Toll for Hierarchical Design and Simulation of Concurrent Systems, Proceedings of the BCS-FACS Workshop on Specification and Verification of Concurrent Systems, p.140-152, July 06-08, 1988
	20	R. Milner, Communication and concurrency, Prentice-Hall, Inc., Upper Saddle River, NJ, 1989
	21	Alexander Moshe Rabinovich, Checking Equivalences Between Concurrent Systems of Finite Agents (Extended Abstract), Proceedings of the 19th International Colloquium on Automata, Languages and Programming, p.696-707, July 13-17, 1992
	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.
	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.
	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.
	25	W. J. Yeh. Controlling State Explosion in Reachability Analysis, Technical Report, SERC-TR-147-P, SERC, Purdue University, December 1993.
	26	Wei Jen Yeh , Michal Young, Compositional reachability analysis using process algebra, Proceedings of the symposium on Testing, analysis, and verification, p.49-59, October 08-10, 1991, Victoria, British Columbia, Canada [doi>10.1145/120807.120812]
	27	W. J. Yeh and M. Young, "Hierarchical Tracing of Concurrent Programs,"Presented at 3rd Irvine Software Symposium (ISS93), Irvine, California, April 1993.

CITED BY 10

	André van der Hoek , Dennis Heimbigner , Alexander L. Wolf, Versioned software architecture, Proceedings of the third international workshop on Software architecture, p.73-76, November 01-05, 1998, Orlando, Florida, United States
	Dimitra Giannakopoulou , Jeff Magee , Jeff Kramer, Checking progress with action priority: is it fair?, ACM SIGSOFT Software Engineering Notes, v.24 n.6, p.511-527, Nov. 1999
	Gleb Naumovich , Lori A. Clarke, Classifying properties: an alternative to the safety-liveness classification, ACM SIGSOFT Software Engineering Notes, v.25 n.6, p.159-168, Nov. 2000
	Shing Chi Cheung , Jeff Kramer, Checking safety properties using compositional reachability analysis, ACM Transactions on Software Engineering and Methodology (TOSEM), v.8 n.1, p.49-78, Jan. 1999
	Fei Xie , James C. Browne, Verified systems by composition from verified components, ACM SIGSOFT Software Engineering Notes, v.28 n.5, September 2003
	K. Suzanne Barber , Tom Graser , Jim Holt, Evaluating dynamic correctness properties of domain reference architectures, Journal of Systems and Software, v.68 n.3, p.217-231, 15 December 2003
	S. Chouali , J. Julliand , P.-A. Masson , F. Bellegarde, PLTL-partitioned model checking for reactive systems under fairness assumptions, ACM Transactions on Embedded Computing Systems (TECS), v.4 n.2, p.267-301, May 2005
	Dimitra Giannakopoulou , Jeff Kramer , Shing Chi Cheung, Behaviour Analysis of Distributed Systems Using the Tracta Approach, Automated Software Engineering, v.6 n.1, p.7-35, January 1999
	Jeff Magee , Jeff Kramer , Dimitra Giannakopoulou, Software Architecture Directed Behaviour Analysis, Proceedings of the 9th international workshop on Software specification and design, p.144, April 16-18, 1998
	Ayaz Isazadeh , Jaber Karimpour, A new formalism for mathematical description and verification of component-based systems, The Journal of Supercomputing, v.49 n.3, p.334-353, September 2009