Article

Invariants and state in testing and formal methods

Author:

Dick HamletAuthors Info & Claims

PASTE '05: Proceedings of the 6th ACM SIGPLAN-SIGSOFT workshop on Program analysis for software tools and engineering

Pages 48 - 51

https://doi.org/10.1145/1108792.1108806

Published: 05 September 2005 Publication History

Get Access

Abstract

Logical formulas called invariants are a staple of formal methods for program analysis. Persistent-state variables appear in these formulas playing their proper intuitive role, which is somewhere between inputs and internal variables. In software testing theory, on the contrary, state is not usually accorded explicit treatment. Comparing the viewpoints of formal methods and testing theory suggests new roles that formal methods can play in testing. This examination is motivated by recent systems such as Daikon, which use both tests and invariants.

References

[1]

M. D. Ernst, J. Cockrell, W. G. Griswold, and D. Notkin. Dynamically discovering likely program invariants to support program evolution. IEEE Trans. on Soft. Eng., pages 99--123, February 2001.

Digital Library

Google Scholar

[2]

Robert W. Floyd. Assigning meanings to programs. In Proceedings Symposium Applied Mathematics, volume 19, pages 19--32. Amer. Math. Soc, 1967.

Crossref

Google Scholar

[3]

Matthew M Geller. Test data as an aid in proving program correctness. Comm. of the ACM, pages 368--375, May 1978.

Digital Library

Google Scholar

[4]

John B. Goodenough and Susan L. Gerhart. Toward a theory of test data selection. In Proceedings of the international conference on Reliable software, pages 493--510, 1975.

Digital Library

Google Scholar

[5]

Neelam Gupta and Zachary V. Heidepriem. A new structural coverage criterion for dynamic detection of program invariants. In ASE 2003: Proceedings of the 18th Annual International Conference on Automated Software Engineering, pages 49--58, San Diego, CA, USA, October 8--10, 2003.

Crossref

Google Scholar

[6]

J. Henkel and A. Diwan. Discovering algebraic specifications from java classes. In Proceedings ECOOP '03, Darmstad, 2003. The authors recommend www-plan.cs.colorado.edu/henkel because the proceedings is garbled.

Google Scholar

[7]

C. A. R. Hoare. An axiomatic basis for computer programming. Comm. of the ACM, pages 576--585, October 1969.

Digital Library

Google Scholar

[8]

D. Marinov and S. Khurshid. Testera: a novel framework for automated testing of java programs. In Proceedings 16th IEEE Int. Conf. on Automated Software Engineering, pages 22--34, San Diego, 2001.

Digital Library

Google Scholar

[9]

David S. Rosenblum. A practical approach to programming with assertions. IEEE Trans. on Soft. Eng., 21:19--31, 1995.

Digital Library

Google Scholar

[10]

Tao Xie and David Notkin. Tool-assisted unit test generation and selection based on operational abstractions. Automated Software Engineering Journal, 2006.

Digital Library

Google Scholar

Cited By

View all

Hamlet D(2015)Theory of Software Testing With Persistent StateIEEE Transactions on Reliability10.1109/TR.2015.243644364:3(1098-1115)Online publication date: Sep-2015
https://doi.org/10.1109/TR.2015.2436443
Herbert DSundaram VLu YBagchi SLi Z(2007)Adaptive correctness monitoring for wireless sensor networks using hierarchical distributed run-time invariant checkingACM Transactions on Autonomous and Adaptive Systems10.1145/1278460.12784622:3(8-es)Online publication date: 1-Sep-2007
https://dl.acm.org/doi/10.1145/1278460.1278462
Kulik TDongol BLarsen PMacedo HSchneider STran-Jørgensen PWoodcock J(2022)A Survey of Practical Formal Methods for SecurityFormal Aspects of Computing10.1145/352258234:1(1-39)Online publication date: 5-Jul-2022
https://dl.acm.org/doi/10.1145/3522582

Index Terms

Invariants and state in testing and formal methods
1. Software and its engineering
2. Theory of computation
  1. Semantics and reasoning
    1. Program reasoning
      1. Invariants

Recommendations

Invariants and state in testing and formal methods

Logical formulas called invariants are a staple of formal methods for program analysis. Persistent-state variables appear in these formulas playing their proper intuitive role, which is somewhere between inputs and internal variables. In software ...
Formal mutation testing for Circus

Context: The demand from industry for more dependable and scalable test-development mechanisms has fostered the use of formal models to guide the generation of tests. Despite many advancements having been obtained with state-based models, such as Finite ...
Formal testing from timed finite state machines

In this paper we present a formal methodology to test both the functional and temporal behaviors in systems where temporal aspects are critical. We extend the classical finite state machines model with features to represent timed systems. Our formalism ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

PASTE '05: Proceedings of the 6th ACM SIGPLAN-SIGSOFT workshop on Program analysis for software tools and engineering

September 2005

118 pages

ISBN:1595932399

DOI:10.1145/1108792

Editors:
Michael Ernst
MIT
,
Thomas Jensen
CNRS

ACM SIGSOFT Software Engineering Notes Volume 31, Issue 1
January 2006
203 pages
ISSN:0163-5948
DOI:10.1145/1108768
Issue’s Table of Contents

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 05 September 2005

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Article

Conference

PASTE05

Sponsor:

PASTE05: PASTE '05 - ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering

September 5 - 6, 2005

Lisbon, Portugal

Acceptance Rates

Overall Acceptance Rate 57 of 159 submissions, 36%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

3
Total Citations
View Citations
395
Total Downloads

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

Reflects downloads up to 23 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Hamlet D(2015)Theory of Software Testing With Persistent StateIEEE Transactions on Reliability10.1109/TR.2015.243644364:3(1098-1115)Online publication date: Sep-2015
https://doi.org/10.1109/TR.2015.2436443
Herbert DSundaram VLu YBagchi SLi Z(2007)Adaptive correctness monitoring for wireless sensor networks using hierarchical distributed run-time invariant checkingACM Transactions on Autonomous and Adaptive Systems10.1145/1278460.12784622:3(8-es)Online publication date: 1-Sep-2007
https://dl.acm.org/doi/10.1145/1278460.1278462
Kulik TDongol BLarsen PMacedo HSchneider STran-Jørgensen PWoodcock J(2022)A Survey of Practical Formal Methods for SecurityFormal Aspects of Computing10.1145/352258234:1(1-39)Online publication date: 5-Jul-2022
https://dl.acm.org/doi/10.1145/3522582

View Options

Login options

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

Cited By

Index Terms

Recommendations

Invariants and state in testing and formal methods

Formal mutation testing for Circus

Formal testing from timed finite state machines