Article

Free access

Classifying properties: an alternative to the safety-liveness classification

Authors:

Gleb Naumovich,

Lori A. ClarkeAuthors Info & Claims

SIGSOFT '00/FSE-8: Proceedings of the 8th ACM SIGSOFT international symposium on Foundations of software engineering: twenty-first century applications

Pages 159 - 168

https://doi.org/10.1145/355045.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.

Digital Library

[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.

Digital Library

[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.

Digital Library

[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

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
Show More Cited By

Recommendations

Classifying properties: an alternative to the safety-liveness classification

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 Conferences

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

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

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]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 November 2000

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Article

Conference

SOFT'00/FSE'00

Sponsor:

SOFT'00/FSE'00: 8th SIGSOFT Symposium on Foundation of Software Engineering

November 6 - 10, 2000

California, San Diego, USA

Acceptance Rates

Overall Acceptance Rate 17 of 128 submissions, 13%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

6
Total Citations
View Citations
545
Total Downloads

Downloads (Last 12 months)53
Downloads (Last 6 weeks)7

Reflects downloads up to 29 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

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
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

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

Media

Figures

Other

Tables

View Table of Contents