A practical method for verifying event-driven software

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

A practical method for verifying event-driven software

Full text

Pdf (1.40 MB)

Source

International Conference on Software Engineering archive
Proceedings of the 21st international conference on Software engineering table of contents

Los Angeles, California, United States

Pages: 597 - 607

Year of Publication: 1999

ISBN:1-58113-074-0

Authors

Gerard J. Holzmann	Bell Laboratories, 2C-521, 600 Mountain Avenue, Murray Hill, NJ
Margaret H. Smith	Bell Laboratories, 2C-406, 600 Mountain Avenue, Murray Hill, NJ

Sponsors

IEEE-CS : Computer Society
IEEE-CS\TCSE : TC on Software Engineering
SIGADA: ACM Special Interest Group on Ada Programming Language
SIGSOFT: ACM Special Interest Group on Software Engineering
SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 17, Downloads (12 Months): 47, Citation Count: 22

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/302405.302710 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	K. A. Bartlett , R. A. Scantlebury , P. T. Wilkinson, A note on reliable full-duplex transmission over half-duplex links, Communications of the ACM, v.12 n.5, p.260-261, May 1969 [doi>10.1145/362946.362970]
	2	Bellcore LSSGR, LATA Switching Systems Generic Requirements, FR-NWT-000064, 1992. Incl: SPCS Capabilities and Features, SR-504: 1, (March 1996).
	3	LSSGR, FSD 01-02-1450, p. 8.
	4	LSSGR, FSD 01-02-1201, p. 2.
	5	Buchi, J.R., "On a decision method in restricted secondorder arithmetics," Proc. 1960 Int. Cong. on Logic, Methods, and Philosophy of Science, Stanford University Press, (1962), pp. 1-12.
	6	William Chan , Richard J. Anderson , Paul Beame , Steve Burns , Francesmary Modugno , David Notkin , Jon D. Reese, Model Checking Large Software Specifications, IEEE Transactions on Software Engineering, v.24 n.7, p.498-520, July 1998 [doi>10.1109/32.708566]
	7	John A. Chaves, Formal Methods at AT&T - An Industrial Usage Report, Proceedings of the IFIP TC6/WG6.1 Fourth International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols: Formal Description Techniques, IV, p.83-90, November 19-22, 1991
	8	Christopher Colby , Patrice Godefroid , Lalita Jategaonkar Jagadeesan, Automatically closing open reactive programs, Proceedings of the ACM SIGPLAN 1998 conference on Programming language design and implementation, p.345-357, June 17-19, 1998, Montreal, Quebec, Canada
	9	Matthew B. Dwyer , George S. Avrunin , James C. Corbett, Property specification patterns for finite-state verification, Proceedings of the second workshop on Formal methods in software practice, p.7-15, March 04-05, 1998, Clearwater Beach, Florida, United States [doi>10.1145/298595.298598]
	10	Rob Gerth , Doron Peled , Moshe Y. Vardi , Pierre Wolper, Simple on-the-fly automatic verification of linear temporal logic, Proceedings of the Fifteenth IFIP WG6.1 International Symposium on Protocol Specification, Testing and Verification XV, p.3-18, June 01, 1995
	11	Patrice Godefroid, VeriSoft: A Tool for the Automatic Analysis of Concurrent Reactive Software, Proceedings of the 9th International Conference on Computer Aided Verification, p.476-479, June 22-25, 1997
	12	C. A. R. Hoare, Communicating sequential processes, Communications of the ACM, v.21 n.8, p.666-677, Aug. 1978 [doi>10.1145/359576.359585]
	13	Holzmann, G.J., "The Theory and Practice of a Formal Method: NewCoRe," Proc. ZFIP World Computer Congress, Vol. I, Hamburg, Germany, (August 1994), pp. 35- 44 North-Holland Publ.
	14	Gerard J. Holzmann, The Model Checker SPIN, IEEE Transactions on Software Engineering, v.23 n.5, p.279-295, May 1997 [doi>10.1109/32.588521]
	15	Marick, B., The Craft of Software Testing, Prentice Hall, (1995), Englewood Cliffs, NJ, USA.
	16	Pnueli, A., "The temporal logic of programs," Proc. 18th IEEE Symposium on Foundations of Computer Science, Providence, R.I.,.(1977), pp. 46-57.
	17	Jared R. W. Smith , Rick Reed, Telecommunications Systems Engineering Using SDL, Elsevier Science Inc., New York, NY, 1989

CITED BY 22

	Muffy Calder , Alice Miller, Using SPIN for feature interaction analysis—a case study, Proceedings of the 8th international SPIN workshop on Model checking of software, p.143-162, May 2001, Toronto, Ontario, Canada
	William Visser , SeungJoon Park , John Penix, Using predicate abstraction to reduce object-oriented programs for model checking, Proceedings of the third workshop on Formal methods in software practice, p.3-182, August 2000, Portland, Oregon, United States
	Satish Chandra , Patrice Godefroid , Christopher Palm, Software model checking in practice: an industrial case study, Proceedings of the 24th International Conference on Software Engineering, May 19-25, 2002, Orlando, Florida
	Muffy Calder , Mario Kolberg , Evan H. Magill , Stephan Reiff-Marganiec, Feature interaction: a critical review and considered forecast, Computer Networks: The International Journal of Computer and Telecommunications Networking, v.41 n.1, p.115-141, 15 January 2003
	Klaus Havelund , Grigore Roşu, An Overview of the Runtime Verification Tool Java PathExplorer, Formal Methods in System Design, v.24 n.2, p.189-215, March 2004
	Marsha Chechik , Wei Ding, Lightweight reasoning about program correctness, Proceedings of the 2001 conference of the Centre for Advanced Studies on Collaborative research, p.1, November 05-07, 2001, Toronto, Ontario, Canada
	Sanjeev Kumar , Kai Li, Using model checking to debug device firmware, ACM SIGOPS Operating Systems Review, v.36 n.SI, Winter 2002
	Abhik Roychoudhury , Tulika Mitra, Specifying multithreaded Java semantics for program verification, Proceedings of the 24th International Conference on Software Engineering, May 19-25, 2002, Orlando, Florida
	Sanjeev Kumar , Kai Li, Using model checking to debug device firmware, Proceedings of the 5th symposium on Operating systems design and implementation Due to copyright restrictions we are not able to make the PDFs for this conference available for downloading , December 09-11, 2002, Boston, Massachusetts
	Barbara Staudt Lerner, Verifying process models built using parameterized state machines, ACM SIGSOFT Software Engineering Notes, v.29 n.4, July 2004
	Patrice Godefroid, Software Model Checking: The VeriSoft Approach, Formal Methods in System Design, v.26 n.2, p.77-101, March 2005
	A. Miller , M. Calder , A. F. Donaldson, A template-based approach for the generation of abstractable and reducible models of featured networks, Computer Networks: The International Journal of Computer and Telecommunications Networking, v.51 n.2, p.439-455, February, 2007
	Alice Miller , Alastair Donaldson , Muffy Calder, Symmetry in temporal logic model checking, ACM Computing Surveys (CSUR), v.38 n.3, p.8-es, 2006
	Muffy Calder , Alice Miller, Feature interaction detection by pairwise analysis of LTL properties: a case study, Formal Methods in System Design, v.28 n.3, p.213-261, May 2006
	Saddek Bensalem , Jean-Claude Fernandez , Klaus Havelund , Laurent Mounier, Confirmation of deadlock potentials detected by runtime analysis, Proceeding of the 2006 workshop on Parallel and distributed systems: testing and debugging, July 17-17, 2006, Portland, Maine, USA
	Miguel Valero Espada , Jaco Van Pol, An abstract interpretation toolkit for μCRL, Formal Methods in System Design, v.30 n.3, p.249-273, June 2007
	Grigore Roşu , Klaus Havelund, Rewriting-Based Techniques for Runtime Verification, Automated Software Engineering, v.12 n.2, p.151-197, April 2005
	Marsha Chechik , Wei Ding, Lightweight Reasoning about Program Correctness, Information Systems Frontiers, v.4 n.4, p.363-377, December 2002
	Youssef Hanna, SLEDE: lightweight verification of sensor network security protocol implementations, The 6th Joint Meeting on European software engineering conference and the ACM SIGSOFT symposium on the foundations of software engineering: companion papers, September 03-07, 2007, Dubrovnik, Croatia
	Youssef Hanna, SLEDE: lightweight verification of sensor network security protocol implementations, Proceedings of the the 6th joint meeting of the European software engineering conference and the ACM SIGSOFT symposium on The foundations of software engineering, September 03-07, 2007, Dubrovnik, Croatia
	María del Mar Gallardo , Jesús Martínez , Pedro Merino , Ernesto Pimentel, On The Evolution Of Reliability Methods For Critical Software, Journal of Integrated Design & Process Science, v.10 n.4, p.55-67, December 2006
	Jean-Baptiste Voron , Fabrice Kordon, Transforming sources to petri nets: a way to analyze execution of parallel programs, Proceedings of the 1st international conference on Simulation tools and techniques for communications, networks and systems & workshops, March 03-07, 2008, Marseille, France