Article

Dynamically inferring temporal properties

Authors:

David EvansAuthors Info & Claims

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

Pages 23 - 28

https://doi.org/10.1145/996821.996832

Published: 07 June 2004 Publication History

Abstract

Model checking requires a specification of the target system's desirable properties, some of which are temporal. Formulating a temporal property of the system based on either its abstract model or implementation requires a deep understanding of its behavior and sophisticated knowledge of the chosen formalism. This has been a major impediment to documenting and verifying temporal properties. We propose a dynamic approach to automatically infer a program's temporal properties based on a set of property pattern templates. We describe a preliminary implementation of this approach, and report on our experience using it to discover interesting temporal properties of a small program.

References

[1]

G. Ammons, R. Bodik, and J. R. Larus. Mining specifications. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '02), January 2002.

Digital Library

[2]

G. Ammons, D. Mandelin, R. Bodik, and J. R. Larus. Debugging temporal specifications with concept analysis. In SIGPLAN Conference on Programming Language Design and Implementation, June 2003.

Digital Library

[3]

T. Ball and S. K. Rajamani. Automatically validating temporal safety properties of interfaces. In 8th International SPIN Workshop on Model Checking of Software, May 2001.

Digital Library

[4]

G. Brat, K. Havelund, S. Park, and W. Visser. Model checking programs. In 15th IEEE International Conference on Automated Software Engineering, September 2000.

Digital Library

[5]

J. E. Cook, Z. Du, C. Liu, and A. L. Wolf. Discovering models of behavior for concurrent systems. New Mexico State University Technical Report, NMSU-CSTR-2002-010.

[6]

J. Corbett, M. Dwyer, J. Hatcliff, S. Laubach, C. Pasareanu, Robby, H. Zheng. Bandera: extracting finite-state models from Java source code. In 22nd International Conference on Software Engineering, June 2000.

Digital Library

[7]

J. Corbett, M. Dwyer, and J. Hatcliff, and Robby. Expressing checkable properties of dynamic systems: the Bandera specification language. KSU CIS Technical Report 2001 -04, Kansas State University, 2001.

[8]

M. Dwyer, G. Avrunin, and J. Corbett. Patterns in property specifications for finite-state verification. In 21 st International Conference on Software Engineering, May 1999.

Digital Library

[9]

M. D. Ernst, J. Cockrell, W. G. Griswold, and D. Notkin. Dynamically discovering likely program invariants to support program evolution. In IEEE Transactions on Software Engineering, February 2001.

Digital Library

[10]

G. J. Holzmann. The model checker Spin. In IEEE Transactions on Software Engineering, May 1997.

Digital Library

[11]

G. J. Holzmann. The logic of bugs. In 10th ACM SIGSOFT International Symposium on Foundations of Software Engineering, November 2002.

Digital Library

[12]

K. Havelund and T. Pressburger. Model checking Java programs using Java PathFinder. In International Journal on Software Tools for Technology Transfer, September 1999.

[13]

K. Havelund. Using runtime analysis to guide model checking of Java programs. In 7th International SPIN Workshop on Model Checking of Software, August/September 2000.

Digital Library

[14]

J. W. Nimmer and M. D. Ernst. Invariant inference for static checking: an empirical evaluation. In ACM SIGSOFT 10th International Symposium on the Foundations of Software Engineering, November 2002.

Digital Library

[15]

K. M. Olender and L. J. Osterweil. Cecil: a sequencing constraint language for automatic static analysis generation. In IEEE Transactions on Software Engineering, March 1990.

Digital Library

[16]

A. Pnueli. The temporal logic of programs. In 18th Annual Symposium on Foundations of Computer Science, October/November 1977.

Digital Library

[17]

J. Whaley, M. C. Martin, and M. S. Lam. Automatic extraction of object-oriented component interfaces. In International Symposium on Software Testing and Analysis, July 2002.

Digital Library

Cited By

Song YGao XLi WChin WRoychoudhury A(2024)ProveNFix: Temporal Property-Guided Program RepairProceedings of the ACM on Software Engineering10.1145/36437371:FSE(226-248)Online publication date: 12-Jul-2024
https://dl.acm.org/doi/10.1145/3643737
Farahmandpour ZSeyedmahmoudian MStojcevski A(2021)A Review on the Service Virtualisation and Its Structural PillarsApplied Sciences10.3390/app1105238111:5(2381)Online publication date: 8-Mar-2021
https://doi.org/10.3390/app11052381
Mahato PNarayan A(2021)MINTS: Unsupervised Temporal Specifications Miner2021 IEEE 21st International Conference on Software Quality, Reliability and Security (QRS)10.1109/QRS54544.2021.00093(841-851)Online publication date: Dec-2021
https://doi.org/10.1109/QRS54544.2021.00093
Show More Cited By

Index Terms

Dynamically inferring temporal properties

Recommendations

A compositional automata-based semantics and preserving transformation rules for testing property patterns
Abstract
Dwyer et al. provide a language to specify dynamic properties based on a limited number of predefined patterns and scopes. The semantics of these properties is defined by translating each combination of a pattern and a scope into usual temporal ...
Specifying and Monitoring Temporal Properties in Web Services Compositions
ECOWS '09: Proceedings of the 2009 Seventh IEEE European Conference on Web Services

Current Web service composition approaches and languages such as WS-BPEL do not allow to define temporal constraints in a declarative and separate way. Also it is not possible to verify if there are contradictions between the temporal constraints ...
Checking temporal properties under simulation of executable system descriptions
HLDVT '00: Proceedings of the IEEE International High-Level Validation and Test Workshop (HLDVT'00)

The verification of systems, i.e., hardware or hardware/software systems, is an important task in the design process. More than 70% of the development time is spend for locating and correcting error in the design. Therefore, many techniques have been ...

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences

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

June 2004

64 pages

ISBN:1581139101

DOI:10.1145/996821

Conference Chairs:
Cormac Flanagan
University of California at Santa Cruz
,
Andreas Zeller
Saarland University

Copyright © 2004 ACM.

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]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 07 June 2004

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Conference

PASTE04

Sponsor:

PASTE04: PASTE '04 - ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering ( co-located with PLDI 2004 Conference )

June 7 - 8, 2004

Washington DC, USA

Acceptance Rates

PASTE '04 Paper Acceptance Rate 10 of 37 submissions, 27%;

Overall Acceptance Rate 57 of 159 submissions, 36%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

46
Total Citations
View Citations
500
Total Downloads

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

Reflects downloads up to 23 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Song YGao XLi WChin WRoychoudhury A(2024)ProveNFix: Temporal Property-Guided Program RepairProceedings of the ACM on Software Engineering10.1145/36437371:FSE(226-248)Online publication date: 12-Jul-2024
https://dl.acm.org/doi/10.1145/3643737
Farahmandpour ZSeyedmahmoudian MStojcevski A(2021)A Review on the Service Virtualisation and Its Structural PillarsApplied Sciences10.3390/app1105238111:5(2381)Online publication date: 8-Mar-2021
https://doi.org/10.3390/app11052381
Mahato PNarayan A(2021)MINTS: Unsupervised Temporal Specifications Miner2021 IEEE 21st International Conference on Software Quality, Reliability and Security (QRS)10.1109/QRS54544.2021.00093(841-851)Online publication date: Dec-2021
https://doi.org/10.1109/QRS54544.2021.00093
Pal DOffenberger SVasudevan S(2020)Assertion Ranking Using RTL Source Code AnalysisIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems10.1109/TCAD.2019.292137439:8(1711-1724)Online publication date: Aug-2020
https://doi.org/10.1109/TCAD.2019.2921374
Mahato PNarayan A(2020)QMine: A Framework for Mining Quantitative Regular Expressions from System Traces2020 IEEE 20th International Conference on Software Quality, Reliability and Security Companion (QRS-C)10.1109/QRS-C51114.2020.00070(370-377)Online publication date: Dec-2020
https://doi.org/10.1109/QRS-C51114.2020.00070
Narayan AFischmeister S(2019)Mining Time for Timed Regular Specifications2019 IEEE International Conference on Systems, Man and Cybernetics (SMC)10.1109/SMC.2019.8914490(63-69)Online publication date: Oct-2019
https://doi.org/10.1109/SMC.2019.8914490
Narayan ACutulenco GJoshi YFischmeister S(2018)Mining Timed Regular Specifications from System TracesACM Transactions on Embedded Computing Systems10.1145/314766017:2(1-21)Online publication date: 3-Jan-2018
https://dl.acm.org/doi/10.1145/3147660
Schmidt LNarayan AFischmeister SRosu GDi Penta MNguyen T(2017)TREM: a tool for mining timed regular specifications from system tracesProceedings of the 32nd IEEE/ACM International Conference on Automated Software Engineering10.5555/3155562.3155675(901-906)Online publication date: 30-Oct-2017
https://dl.acm.org/doi/10.5555/3155562.3155675
Schmidt LNarayan AFischmeister S(2017)TREM: A tool for mining timed regular specifications from system traces2017 32nd IEEE/ACM International Conference on Automated Software Engineering (ASE)10.1109/ASE.2017.8115702(901-906)Online publication date: Oct-2017
https://doi.org/10.1109/ASE.2017.8115702
Cutulenco GJoshi YNarayan AFischmeister SLi MWang XLucia (2016)Mining timed regular expressions from system tracesProceedings of the 5th International Workshop on Software Mining10.1145/2975961.2975962(3-10)Online publication date: 3-Sep-2016
https://dl.acm.org/doi/10.1145/2975961.2975962
Show More Cited By

View Options

Login options

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

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents