Property specification patterns for finite-state verification

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Property specification patterns for finite-state verification

Full text

Pdf (1.05 MB)

Source

Formal Methods in Software Practice archive
Proceedings of the second workshop on Formal methods in software practice table of contents

Clearwater Beach, Florida, United States

Pages: 7 - 15

Year of Publication: 1998

ISBN:0-89791-954-8

Authors

Matthew B. Dwyer	Kansas State University, Department of Computing and Information Sciences, 234 Nichols Hall Manhattan, KS
George S. Avrunin	University of Massachusetts, Department of Mathematics and Statistics, Box 34515, Amherst, MA
James C. Corbett	University of Hawai'i, Department of Information and Computer Science, Honolulu, HI

Sponsor

SIGSOFT: ACM Special Interest Group on Software Engineering

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 19, Downloads (12 Months): 80, Citation Count: 21

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/298595.298598 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	Richard J. Anderson , Paul Beame , Steve Burns , William Chan , Francesmary Modugno , David Notkin , Jon D. Reese, Model checking large software specifications, ACM SIGSOFT Software Engineering Notes, v.21 n.6, p.156-166, Nov. 1996
	2	B. Appleton. Patterns and Software: Essential Concepts and Terminology. http://wJw, enteract, co~/ -bradapp/docs/patterns- intro .ht~L~, 1997.
	3	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]
	4	Frank Buschmann , Regine Meunier , Hans Rohnert , Peter Sommerlad , Michael Stal, Pattern-oriented software architecture: a system of patterns, John Wiley & Sons, Inc., New York, NY, 1996
	5	B. G. Cain, J. O. Coplien, and N. B. Harrison. Social Patterns in Productive Software Organizations. Annals of Software Engineering, 2:259-286, Dec. 1996.
	6	Albert Timothy Chamillard , Lori A. Clarke, An empirical comparison of static concurrency analysis techniques, 1996
	7	E. M. Clarke , E. A. Emerson , A. P. Sistla, Automatic verification of finite-state concurrent systems using temporal logic specifications, ACM Transactions on Programming Languages and Systems (TOPLAS), v.8 n.2, p.244-263, April 1986 [doi>10.1145/5397.5399]
	8	Rance Cleaveland , Joachim Parrow , Bernhard Steffen, The concurrency workbench: a semantics-based tool for the verification of concurrent systems, ACM Transactions on Programming Languages and Systems (TOPLAS), v.15 n.1, p.36-72, Jan. 1993 [doi>10.1145/151646.151648]
	9	J. Coplien. Organizational Patterns. http: //www. bell- 1 abs. corn/cg i-user/0rgP ate erns/ OrgPatt erns? 0rganizat iona~lPatt erns, 1997.
	10	James O. Coplien , Douglas C. Schmidt, Pattern languages of program design, ACM Press/Addison-Wesley Publishing Co., New York, NY, 1995
	11	James C. Corbett , George S. Avrunin, Using integer programming to verify general safety and liveness properties, Formal Methods in System Design, v.6 n.1, p.97-123, Jan. 1995 [doi>10.1007/BF01384316]
	12	L. K. Dillon , G. Kutty , L. E. Moser , P. M. Melliar-Smith , Y. S. Ramakrishna, A graphical interval logic for specifying concurrent systems, ACM Transactions on Software Engineering and Methodology (TOSEM), v.3 n.2, p.131-165, April 1994 [doi>10.1145/192218.192226]
	13	M. Dwyer, G. Avrnnin, and J. Corbett. A System of Specification Patterns. http://wee, ciz.ksu, edu/ ~deyer/spec-pattern~. htJLl, 1997.
	14	Matthew B. Dwyer , Vicki Carr , Laura Hines, Model checking graphical user interfaces using abstractions, Proceedings of the 6th European conference held jointly with the 5th ACM SIGSOFT international symposium on Foundations of software engineering, p.244-261, September 22-25, 1997, Zurich, Switzerland
	15	Matthew B. Dwyer , Lori A. Clarke, Data flow analysis for verifying properties of concurrent programs, ACM SIGSOFT Software Engineering Notes, v.19 n.5, p.62-75, Dec. 1994
	16	Martin Fowler, Analysis patterns: reusable objects models, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1996
	17	Erich Gamma , Richard Helm , Ralph Johnson , John Vlissides, Design patterns: elements of reusable object-oriented software, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1995
	18	Z. Har'E1 and R. P. Kurshan. Software for analyti- Technical Journal, 69(1):44-59, 1990.
	19	David C. Hay, Data Model Patterns: Conventions of Thought, Dorset House Publishing Co., Inc., New York, NY, 2000
	20	L. Lamport. Proving the correctness of multiprocess programs. IEEE Transactions on Software Engineerins, SF_,-3(2):125-143, 1977.
	21	Zohar Manna , Amir Pnueli, The temporal logic of reactive and concurrent systems, Springer-Verlag New York, Inc., New York, NY, 1992
	22	M. Manns, H. Sharp, P. McLaughlin, and M. Prieto. Pedagogical Patterns: Successes in T~ Object Technology. http://eee.cs.unca.edu/'manns/ oopsla, htJLl, 1997.
	23	Kenneth L. McMillan, Symbolic Model Checking, Kluwer Academic Publishers, Norwell, MA, 1993
	24	Gleb N. Naumovich , Lori A. Clarke , Leon J. Osterweil, Verification of communication protocols using data flow analysis, Proceedings of the 4th ACM SIGSOFT symposium on Foundations of software engineering, p.93-105, October 16-18, 1996, San Francisco, California, United States
	25	Kurt M. Olender , Leon J. Osterweil, Cecil: A Sequencing Constraint Language for Automatic Static Analysis Generation, IEEE Transactions on Software Engineering, v.16 n.3, p.268-280, March 1990 [doi>10.1109/32.48935]
	26	David S. Rosenblum, Formal methods and testing: why the state-of-the art is not the state-of-the practice, ACM SIGSOFT Software Engineering Notes, v.21 n.4, p.64-66, July 1996 [doi>10.1145/232069.232086]
	27	Jeannette M. Wing , Mandana Vaziri-Farahani, Model checking software systems: a case study, ACM SIGSOFT Software Engineering Notes, v.20 n.4, p.128-139, Oct. 1995

CITED BY 21

	Matthew B. Dwyer , George S. Avrunin , James C. Corbett, Patterns in property specifications for finite-state verification, Proceedings of the 21st international conference on Software engineering, p.411-420, May 16-22, 1999, Los Angeles, California, United States
	Gerard J. Holzmann , Margaret H. Smith, A practical method for verifying event-driven software, Proceedings of the 21st international conference on Software engineering, p.597-607, May 16-22, 1999, Los Angeles, California, United States
	Paulo J. F. Carreira , Miguel E. F. Costa, Automatically verifying an object-oriented specification of the steam-boiler system, Science of Computer Programming, v.46 n.3, p.197-217, March 2003
	Matthew B. Dwyer , Corina S. Pasareanu, Filter-based model checking of partial systems, ACM SIGSOFT Software Engineering Notes, v.23 n.6, p.189-202, Nov. 1998
	G. J. Holzmann , M. H. Smith, An Automated Verification Method for Distributed Systems Software Based on Model Extraction, IEEE Transactions on Software Engineering, v.28 n.4, p.364-377, April 2002
	Alexander Holt , Ewan Klein, A semantically-derived subset of English for hardware verification, Proceedings of the 37th annual meeting of the Association for Computational Linguistics on Computational Linguistics, p.451-456, June 20-26, 1999, College Park, Maryland
	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
	Jaco Geldenhuys , Antti Valmari, More efficient on-the-fly LTL verification with Tarjan's algorithm, Theoretical Computer Science, v.345 n.1, p.60-82, 21 November 2005
	Marieke Huisman , Kerry Trentelman, Factorising temporal specifications, Proceedings of the 2005 Australasian symposium on Theory of computing, p.87-96, January 01, 2005, Newcastle, Australia
	David Berner , Syed Suhaib , Sandeep Kumar Shukla , Jean-Pierre Talpin, XFM: extreme formal method for capturing formal specification into abstract models, Formal methods and models for system design: a system level perspective, Kluwer Academic Publishers, Norwell, MA, 2004
	Rachel L. Smith , George S. Avrunin , Lori A. Clarke , Leon J. Osterweil, PROPEL: an approach supporting property elucidation, Proceedings of the 24th International Conference on Software Engineering, May 19-25, 2002, Orlando, Florida
	Andreas Bauer , Jan Juerjens, Security protocols, properties, and their monitoring, Proceedings of the fourth international workshop on Software engineering for secure systems, p.33-40, May 17-18, 2008, Leipzig, Germany
	Jiří Barnat , Ivana Černá, Distributed breadth-first search LTL model checking, Formal Methods in System Design, v.29 n.2, p.117-134, September 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
	AnnMarie Ericsson , Paul Pettersson , Mikael Berndtsson , Marco Seiriö, Seamless formal verification of complex event processing applications, Proceedings of the 2007 inaugural international conference on Distributed event-based systems, June 20-22, 2007, Toronto, Ontario, Canada
	AnnMarie Ericsson , Mikael Berndtsson, REX, the rule and event eXplorer, Proceedings of the 2007 inaugural international conference on Distributed event-based systems, June 20-22, 2007, Toronto, Ontario, Canada
	George Spanoudakis , Christos Kloukinas , Kelly Androutsopoulos, Towards security monitoring patterns, Proceedings of the 2007 ACM symposium on Applied computing, March 11-15, 2007, Seoul, Korea
	Y. Liu , S. Müller , K. Xu, A static compliance-checking framework for business process models, IBM Systems Journal, v.46 n.2, p.335-361, April 2007
	Charles Pecheur , Franco Raimondi , Guillaume Brat, A formal analysis of requirements-based testing, Proceedings of the eighteenth international symposium on Software testing and analysis, July 19-23, 2009, Chicago, IL, USA
	Franco Raimondi , James Skene , Wolfgang Emmerich, Efficient online monitoring of web-service SLAs, Proceedings of the 16th ACM SIGSOFT International Symposium on Foundations of software engineering, November 09-14, 2008, Atlanta, Georgia
	M. Metzger , A. Anane , F. Rousseau , J. Vachon , E. M. Aboulhamid, Introspection mechanisms for runtime verification in a system-level design environment, Microelectronics Journal, v.40 n.7, p.1124-1134, July, 2009