article

Free access

Classifying properties: an alternative to the safety-liveness classification

Authors:

Gleb Naumovich,

Lori A. ClarkeAuthors Info & Claims

ACM SIGSOFT Software Engineering Notes, Volume 25, Issue 6

Pages 159 - 168

https://doi.org/10.1145/357474.355066

Published: 01 November 2000 Publication History

Abstract

Traditionally, verification properties have been classified as safety or liveness properties. While this taxonomy has an attractive simplicity and is useful for identifying the appropriate analysis algorithm for checking a property, determining whether a property is safety, liveness, or neither can require significant mathematical insight on the part of the analyst. In this paper, we present an alternative property taxonomy. We argue that this taxonomy is a more natural classification of the kinds of questions that analysts want to ask. Moreover, most classes in our taxonomy have a known, direct mapping to the safety-liveness classification, and thus the appropriate analysis algorithm can be automatically determined.

References

[1]

M. Abadi and L. Lamport. Composing specifications. A CM Transactions on Programming Languages and Systems, 15(1):73-132, Jan. 1993.

Digital Library

[2]

S. Aggarwal, C. Courcoubetis, and P. Wolper. Adding liveness properties to coupled finite-state machines. ACM Transactions of Programming Languages and Systems, 12(2):303- 339, Apr. 1990.

Digital Library

[3]

B. Alpem and F. B. Schneider. Defining liveness. Information Processing Letters, 21(4):181-185, Oct. 1985.

[4]

B. Alpern and E B. Schneider. Recognizing safety and livehess. Distributed Computing, 2:117-126, 1987.

Digital Library

[5]

B. Alpem and F. B. Schneider. Verifying temporal properties without temporal logic. ACM Transactions of Programming Languages and Systems, 11(1):147-167, Jan. 1989.

Digital Library

[6]

S. C. Cheung, D. Giannakopoulou, and J. Kramer. Verification of liveness properties using compositional reachability analysis. In Proceedings of the 6th European Software Engineering Conference and 5th ACM SIGSOFT Symposium on the Foundations of Software Engineering, pages 227-243, Sept. 1997.

Digital Library

[7]

S.C. Cheung and J. Kramer. Checking safety properties using compositional reachability analysis. ACM Transactions on Software Engineering and Methodology, 8(1):49-78, Jan. 1999.

Digital Library

[8]

E. M. Clarke, E. A. Emerson, and A. P. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. A CM Transactions of Programming Languages and Systems, 8(2):244-263, Apr. 1986.

Digital Library

[9]

M. B. Dwyer, G. S. Avrunin, and J. C. Corbett. Patterns in property specifications for finite-state verification. In Proceedings of the 21st International Conference on Software Engineering, pages 411-421, May 1999.

Digital Library

[10]

M.B. Dwyer and L. A. Clarke. Data flow analysis for verifying properties of concurrent programs. In Proceedings of the 2nd ACM SIGSOFT Symposium on the Foundations of Software Engineering, pages 62-75, Dec. 1994.

Digital Library

[11]

M. B. Dwyer and L. A. Clarke. Flow analysis for verifying specifications of concurrent and distributed software. Technical Report 1999-52, University of Massachusetts, Amherst, Aug. 1999. f t p ://f t p, ca.umass, edu/pub/techrept/ techreport/1999/UM-CS- 1999-052 .ps.

[12]

P. Godefroid and G. J. Holzmann. On the verification of temporal properties. In Proceedings of the 13th International Conference on Protocol Specification, Testing, and Verification, INWG/IFIP, pages 109-124, May 1993.

Digital Library

[13]

G.J. Holzmann. The model checking SPIN. IEEE Transactions on Software Engineering, 23(5):279-295, May 1997.

Digital Library

[14]

L. Lamport. Proving the correctness of multiprocess programs. IEEE Transactions on Software Engineering, SE- 3(2):125-143, 1977.

Digital Library

[15]

Leslie Lamport. What good is temporal logic? In Proceedings of the IFIP Congress on Information Processing, pages 657-667, 1983.

[16]

Z. Manna and A. Pnueli. Verification of Concurrent Programs: The Temporal Framework, pages 141-154. Academic Press, 1981.

[17]

Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems. Springer, New York, 1992.

[18]

G. Naumovich and L. A. Clarke. Extending FLAVERS to check properties on infinite executions of concurrent software systems. Technical Report 2000-02, Polytechnic University, New York, 2000. http ://cia.poly .edu/tr/ tr-cis-2OOO-O2.pdf.

[19]

K. M. 0lender and L. J. Osterweil. Cecil: A sequencing constraint language for automatic static analysis generation. IEEE Transactions on Software Engineering, 16(3):268-280, Mar. 1990.

Digital Library

[20]

A. Pnueli. The temporal logic of programs. In Proceedings of the 18th Symposium on Foundations of Computer Science, pages 46-57, Oct.-Nov. 1977.

Digital Library

[21]

M. Y. Vardi. Verification of concurrent programs: The automata-theoretic framework. In Proceedings of the 2nd Annual Symposium on Logic in Computer Science, pages 167- 176, June 1987.

[22]

P. Wolper. Temporal logic can be more expressive. Information and Control, 56(1/2):72-99, Jan./Feb. 1983.

Cited By

Stojanovićc L(2007)Ontology-Based Change Management in an eGovernment Application ScenarioSemantic Web Services10.1007/3-540-70894-4_12(339-364)Online publication date: 2007
https://doi.org/10.1007/3-540-70894-4_12
Katoen JSong LZhang LHenzinger TMiller D(2014)Probably safe or liveProceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)10.1145/2603088.2603147(1-10)Online publication date: 14-Jul-2014
https://dl.acm.org/doi/10.1145/2603088.2603147
Montali MTorroni PChesani FMello PAlberti MLamma E(2010)Abductive Logic Programming as an Effective Technology for the Static Verification of Declarative Business ProcessesFundamenta Informaticae10.5555/1890507.1890512102:3-4(325-361)Online publication date: 1-Aug-2010
https://dl.acm.org/doi/10.5555/1890507.1890512
Show More Cited By

Recommendations

Classifying properties: an alternative to the safety-liveness classification
SIGSOFT '00/FSE-8: Proceedings of the 8th ACM SIGSOFT international symposium on Foundations of software engineering: twenty-first century applications

Traditionally, verification properties have been classified as safety or liveness properties. While this taxonomy has an attractive simplicity and is useful for identifying the appropriate analysis algorithm for checking a property, determining whether ...
Classifying Propertie: An Alternative to the Safety-Liveness Classification
On locally checkable properties
LPAR'06: Proceedings of the 13th international conference on Logic for Programming, Artificial Intelligence, and Reasoning

The large computational price of formal verification of general ω-regular properties has led to the study of restricted classes of properties, and to the development of verification methodologies for them. Examples that have been widely accepted by the ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM SIGSOFT Software Engineering Notes

ACM SIGSOFT Software Engineering Notes Volume 25, Issue 6

Nov. 2000

169 pages

ISSN:0163-5948

DOI:10.1145/357474

Editors:
Will Tracz
Lockheed Martin Federal systems, Owego, NY
,
David S. Rosenblum
Univ. of California, Irvine

Issue’s Table of Contents

SIGSOFT '00/FSE-8: Proceedings of the 8th ACM SIGSOFT international symposium on Foundations of software engineering: twenty-first century applications
November 2000
170 pages
ISBN:1581132050
DOI:10.1145/355045
Chairman:
John C. Knight
Univ of Virginia
,
Editor:
David S. Rosenblum
Univ of California, Irvine

Copyright © 2000 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]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 November 2000

Published in SIGSOFT Volume 25, Issue 6

Check for updates

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

6
Total Citations
View Citations
582
Total Downloads

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

Reflects downloads up to 25 Feb 2025

Other Metrics

View Author Metrics

Citations

Cited By

Stojanovićc L(2007)Ontology-Based Change Management in an eGovernment Application ScenarioSemantic Web Services10.1007/3-540-70894-4_12(339-364)Online publication date: 2007
https://doi.org/10.1007/3-540-70894-4_12
Katoen JSong LZhang LHenzinger TMiller D(2014)Probably safe or liveProceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)10.1145/2603088.2603147(1-10)Online publication date: 14-Jul-2014
https://dl.acm.org/doi/10.1145/2603088.2603147
Montali MTorroni PChesani FMello PAlberti MLamma E(2010)Abductive Logic Programming as an Effective Technology for the Static Verification of Declarative Business ProcessesFundamenta Informaticae10.5555/1890507.1890512102:3-4(325-361)Online publication date: 1-Aug-2010
https://dl.acm.org/doi/10.5555/1890507.1890512
Zschaler S(2009)Formal specification of non-functional properties of component-based software systemsSoftware & Systems Modeling10.1007/s10270-009-0115-69:2(161-201)Online publication date: 15-Feb-2009
https://doi.org/10.1007/s10270-009-0115-6
Dwyer MClarke LCobleigh JNaumovich G(2004)Flow analysis for verifying properties of concurrent software systemsACM Transactions on Software Engineering and Methodology10.1145/1040291.104029213:4(359-430)Online publication date: 1-Oct-2004
https://dl.acm.org/doi/10.1145/1040291.1040292
Solaiman EMolina-Jimenez CShrivastav S(2003)Model Checking Correctness Properties of Electronic ContractsService-Oriented Computing – ICSOC 200710.1007/978-3-540-24593-3_21(303-318)Online publication date: 2003
https://doi.org/10.1007/978-3-540-24593-3_21

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

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

Figures

Tables

Media

View Issue’s Table of Contents