Article

Automatic abstraction for model checking software systems with interrelated numeric constraints

Authors:

Sanjai Rayadurgam,

Mats P.E. HeimdahlAuthors Info & Claims

ESEC/FSE-9: Proceedings of the 8th European software engineering conference held jointly with 9th ACM SIGSOFT international symposium on Foundations of software engineering

Pages 164 - 174

https://doi.org/10.1145/503209.503232

Published: 01 September 2001 Publication History

Abstract

Model checking techniques have not been effective in important classes of software systems characterized by large (or infinite) input domains with interrelated linear and non-linear constraints over the input variables. Various model abstraction techniques have been proposed to address this problem. In this paper, we wish to propose domain abstraction based on data equivalence and trajectory reduction as an alternative and complement to other abstraction techniques. Our technique applies the abstraction to the input domain (environment) instead of the model and is applicable to constraint-free and deterministic constrained data transition system. Our technique is automatable with some minor restrictions.

References

[1]

R. Alur, T. Henzinger, and P. Ho. Automatic symbolic verification of embedded systems. IEEE Transactions on Software Engineering, 22(3):181-201, March 1996.]]

Digital Library

[2]

J. Atlee and J. Gannon. State-based model checking of event-driven system requirements. In Proceedings of the ACM SIGSOFT '91 Conference on Software for Critical Systems. Software Engineering Notes. Volume 16 Number 5, 1991.]]

Digital Library

[3]

B. Beizer. Software testing techniques. Van Nostrand Reinhold, New York, 2nd edition, 1990.]]

Digital Library

[4]

B. Boigelot and P. Godefroid. Symbolic verification of communication protocols with infinite state spaces using qdds. Formal Methods and System Design, 14(3):237-255, May 1999.]]

Digital Library

[5]

T. Bultan, R. Gerber, and C. League. Verifying systems with integer constraints and boolean predicates: A composite approach. In Proceedings of ISSTA'98, pages 113-123, march 1998.]]

Digital Library

[6]

T. Bultan, R. Gerber, and W. Pugh. Model-checking concurrent systems with unbounded integer variables: Symbolic representations, approximations, and experimental results. ACM Transactions on Programming Languages and Systems, 21(4):747-789, July 1999.]]

Digital Library

[7]

J. R. Burch, E. M. Clarke, D. E. Long, K. L. McMillan, and D. L. Dill. Symbolic model checking for sequential circuit verification. IEEE Transactions on Computer-AidedDesign of Integrated Circuits and Systems, April 1994.]]

Digital Library

[8]

W. Chan, R. Anderson, P. Beame, S. Burns, F. Modugno, D. Notkin, and J. Reese. Model checking large software specifications. IEEE Transactions on Software Engineering, 24(7):498-520, July 1998.]]

Digital Library

[9]

W. Chan, R. Anderson, P. Beame, and D. Notkin. Combining constraint solving and symbolic model checking for a class of systems with non-linear constraints. In Computer Aided Verification, pages 316-327. Springer Verlag, 1997.]]

[10]

E. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press, 2000.]]

Digital Library

[11]

Constraint logic programming over rational or real. Available at http://www.ai.univie.ac.at/clpqr/.]]

[12]

M. Colon and T. Uribe. Generating finite-state abstractions of reactive systems using decision procedures. In Computer Aided Verification, pages 293-304. Springer, 1998.]]

[13]

D. Dams, O.Grumberg, and R. Gerth. Generation of reduced models for checking fragments of CTL. In Computer Aided Verification, pages 479-490. Springer Verlag, 1993.]]

[14]

S. Das, D. L. Dill, and S. Park. Experience with predicate abstraction. In N. Halbwachs and D. Peled, editors, Proceedings of CAV '99, volume 1633 of LNCS, pages 160-171. Springer-Verlag, July 1999.]]

Digital Library

[15]

E. Emerson and K. Namjoshi. On model checking for non-deterministic infinite-state systems. In Thirteenth Annual IEEE Symposium on Logics in Computer Science, pages 70-80, 1998.]]

Digital Library

[16]

O. Grumberg and D.E.Long. Model checking and modular verification. ACM Transactions on Programming Languages and Systems, 16(3):843-871, May 1994.]]

Digital Library

[17]

J. Hatcliff, M. B. Dwyer, and H. Zheng. Slicing software for model construction. Higher-Order and Symbolic Computation, 13(4):315-353, December 2000.]]

Digital Library

[18]

M. P. Heimdahl, J. M. Thompson, and M. W. Whalen. On the effectiveness of slicing hierarchical state machines: A case study. InProceedings of the Twenty-fourth EUROMICRO Conference, volume 1, pages 435-444, 1998.]]

Digital Library

[19]

C. Heitmeyer, J. Kirby, B. Labaw, M. Archer, and R. Bharadwaj. Using abstraction and model checking to detect safety violations in requirements specifications. IEEE Transactions on Software Engineering, 24(11):927-948, November 1998.]]

Digital Library

[20]

T. A. Henzinger and P.-H. Ho. HyTech: The Cornell Hybrid Technology Tool. In Hybrid Systems II, volume 999 of Lecture Notes in Computer Science, pages 265-294. Springer-Verlag, 1995.]]

[21]

G. J. Holzmann. The model checker S pin . IEEE Transactions on Software Engineering, pages 279-295, May 1997.]]

Digital Library

[22]

Z. Manna, M. Colon, B. Finkbeiner, H. Sipma, and T. Uribe. Abstraction and modular verification of infinite-state reactive systems. In Requirements Targeting Software and Systems Engineering (RTSE), LNCS. Springer Verlag, 1998.]]

Digital Library

[23]

K. L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993.]]

Digital Library

[24]

NuSMV: A New Symbolic Model Checking. Available at http://http://nusmv.irst.itc.it/.]]

[25]

J. M. Thompson, M. P. Heimdahl, and S. P. Miller. Specification based prototyping for embedded systems. In Seventh ACM SIGSOFT Symposium on the Foundations on Software Engineering, volume 1687 of Lecture Notes in Computer Science, pages 163-179, September 1999.]]

Digital Library

[26]

W. Visser, S. Park, and J. Penix. Using predicate abstraction to reduce object-oriented programs for model checking. In Proceedings of the Third ACM Workshop on Formal Methods in Software Practice, pages 3-12, August 2000.]]

Digital Library

[27]

P. Wolper and B. Boigelot. Verifying systems with infinite but regular state spaces. In Computer Aided Verification, pages 88-97. Springer, 1998.]]

[28]

P. Wolper and P. Godefroid. Partial-order methods for temporal verification. In CONCUR'93, volume 715 of LNCS, pages 233-246. Springer-Verlag, 1993.]]

Cited By

Karna AChen YYu HZhong HZhao J(2018)The role of model checking in software engineeringFrontiers of Computer Science: Selected Publications from Chinese Universities10.1007/s11704-016-6192-012:4(642-668)Online publication date: 1-Aug-2018
https://dl.acm.org/doi/10.1007/s11704-016-6192-0
Magill SBerdine JClarke ECook B(2007)Arithmetic strengthening for shape analysisProceedings of the 14th international conference on Static Analysis10.5555/2391451.2391479(419-436)Online publication date: 22-Aug-2007
https://dl.acm.org/doi/10.5555/2391451.2391479
Magill SBerdine JClarke ECook B(2007)Arithmetic Strengthening for Shape AnalysisStatic Analysis10.1007/978-3-540-74061-2_26(419-436)Online publication date: 2007
https://doi.org/10.1007/978-3-540-74061-2_26
Show More Cited By

Index Terms

Automatic abstraction for model checking software systems with interrelated numeric constraints
1. Software and its engineering
  1. Software organization and properties
    1. Software functional properties
      1. Formal methods
        Model checking
2. Theory of computation
  1. Logic
    1. Verification by model checking

Recommendations

Automatic abstraction for model checking software systems with interrelated numeric constraints

Model checking techniques have not been effective in important classes of software systems characterized by large (or infinite) input domains with interrelated linear and non-linear constraints over the input variables. Various model abstraction ...
Automatic abstraction in model checking
Automatic Abstraction in SMT-Based Unbounded Software Model Checking
CAV 2013: Proceedings of the 25th International Conference on Computer Aided Verification - Volume 8044

Software model checkers based on under-approximations and SMT solvers are very successful at verifying safety i.e., reachability properties. They combine two key ideas --- a concreteness: a counterexample in an under-approximation is a counterexample in ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

ESEC/FSE-9: Proceedings of the 8th European software engineering conference held jointly with 9th ACM SIGSOFT international symposium on Foundations of software engineering

September 2001

329 pages

ISBN:1581133901

DOI:10.1145/503209

Conference Chairs:
A. Min Tjoa
Vienna Univ. of Technology, Vienna, Austria
,
Volker Gruhn
Univ. of Dortmund, Dortmund, Germany

ACM SIGSOFT Software Engineering Notes Volume 26, Issue 5
Sept. 2001
329 pages
ISSN:0163-5948
DOI:10.1145/503271
Issue’s Table of Contents

Copyright © 2001 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

CEPIS: Council of European Professional Informatics Societies
VIENUT: Vienna University of Technology
SIGSOFT: ACM Special Interest Group on Software Engineering

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 September 2001

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Conference

ESEC/FSE01

Sponsor:

CEPIS
VIENUT
SIGSOFT

ESEC/FSE01: European Software Engineering Conference 2001/ Foundations on Software Engineering 2001

September 10 - 14, 2001

Vienna, Austria

Acceptance Rates

ESEC/FSE-9 Paper Acceptance Rate 29 of 137 submissions, 21%;

Overall Acceptance Rate 112 of 543 submissions, 21%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

9
Total Citations
View Citations
380
Total Downloads

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

Reflects downloads up to 13 Feb 2025

Other Metrics

View Author Metrics

Citations

Cited By

Karna AChen YYu HZhong HZhao J(2018)The role of model checking in software engineeringFrontiers of Computer Science: Selected Publications from Chinese Universities10.1007/s11704-016-6192-012:4(642-668)Online publication date: 1-Aug-2018
https://dl.acm.org/doi/10.1007/s11704-016-6192-0
Magill SBerdine JClarke ECook B(2007)Arithmetic strengthening for shape analysisProceedings of the 14th international conference on Static Analysis10.5555/2391451.2391479(419-436)Online publication date: 22-Aug-2007
https://dl.acm.org/doi/10.5555/2391451.2391479
Magill SBerdine JClarke ECook B(2007)Arithmetic Strengthening for Shape AnalysisStatic Analysis10.1007/978-3-540-74061-2_26(419-436)Online publication date: 2007
https://doi.org/10.1007/978-3-540-74061-2_26
Heimdahl MChoi YWhalen M(2005)Deviation AnalysisAutomated Software Engineering10.1007/s10515-005-2642-x12:3(321-347)Online publication date: 1-Jul-2005
https://dl.acm.org/doi/10.1007/s10515-005-2642-x
Hsiung PLin STseng CLee TFu JSee W(2004)VERTAFIEEE Transactions on Software Engineering10.1109/TSE.2004.6830:10(656-674)Online publication date: 1-Oct-2004
https://dl.acm.org/doi/10.1109/TSE.2004.68
Heimdahl MRayadurgam SVisser WDevaraj GGao J(2004)Auto-generating Test Sequences Using Model Checkers: A Case StudyFormal Approaches to Software Testing10.1007/978-3-540-24617-6_4(42-59)Online publication date: 2004
https://doi.org/10.1007/978-3-540-24617-6_4
Choi YHeimdahl M(2003)Model checking software requirement specifications using domain reduction abstractionProceedings of the 18th IEEE International Conference on Automated Software Engineering10.1109/ASE.2003.1240328(314-317)Online publication date: 6-Oct-2003
https://dl.acm.org/doi/10.1109/ASE.2003.1240328
Rayadurgam S(2001)Automated Test-Data Generation from Formal Models of SoftwareProceedings of the 16th IEEE international conference on Automated software engineering10.5555/872023.872531Online publication date: 26-Nov-2001
https://dl.acm.org/doi/10.5555/872023.872531
Bernard ELegeard BLuck XPeureux F(2004)Generation of test sequences from formal specificationsSoftware—Practice & Experience10.1002/spe.59734:10(915-948)Online publication date: 1-Aug-2004
https://dl.acm.org/doi/10.1002/spe.597

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.

Figures

Tables

Media

View Table of Conten