Article

Symbolic model checking of declarative relational models

Authors:

Felix Sheng-Ho Chang,

Daniel JacksonAuthors Info & Claims

ICSE '06: Proceedings of the 28th international conference on Software engineering

Pages 312 - 320

https://doi.org/10.1145/1134285.1134329

Published: 28 May 2006 Publication History

Abstract

This paper explores the idea of augmenting traditional model checkers with the expressiveness of a declarative, relational language. The goal is to enable programmers to write very intuitive and compact specifications, in order to allow the automatic verification of more complicated software systems. The key idea is that many structural operations (common in object-oriented programs) can be easily described using relations and relational operators, while other operations are best described using the primitive data types and their operations (such as simple arithmetic operations on numbers). By allowing a mixture of both, and by allowing parts of the model to be described declaratively rather than imperatively, the programmer has the freedom to model each part of the system differently, using the most intuitive and simple constructs. We built a BDD-based model checker for the language, and successfully verified a straightforward model of the dependency algorithm in Apache Ant for up to 5 nodes.

References

[1]

A. Tarski. A lattice-theoretical fixpoint theorem and its applications. In Pacific Journal of Mathematics 5, pages 285--309.

[2]

J. Abrial. The B Book - Assigning Programs to Meanings. Cambridge University Press, 1996.

[3]

Daniel Jackson. Automating First-Order Relational Logic. In Proceedings of the 8th ACM SIGSOFT international symposium on Foundations of software engineering. ACM Press, 2000.

Digital Library

[4]

Daniel Jackson, Ilya Shlyakhter, and Manu Sridharan. A Micromodularity Mechanism. In Proceedings of the ACM SIGSOFT Conference on the Foundations of Software Engineering / European Software Engineering Conference (FSE / ESEC '01), 2001.

Digital Library

[5]

David L. Dill. The Murphi Verification System. In Proceedings of the 8th International Conference on Computer Aided Verification, pages 390--393, 1996.

Digital Library

[6]

David L. Dill, Andreas J. Drexler, Alan J. Hu, and C. Han Yang. Protocol verification as a hardware design aid. In Proceedings of the 8th International Conference on Computer Aided Verification, pages 522--525, 1992.

Digital Library

[7]

E.M. Clarke, E.A. Emerson, and A.P. Sistla. Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications. In ACM Transactions on Programming Languages and Systems (TOPLAS). ACM Press, 1986.

Digital Library

[8]

Gerard J. Holzmann. The Model Checker SPIN. In IEEE Transactions on Software Engineering, Vol. 23, No. 5, 1997.

Digital Library

[9]

Jonathan Edwards, Daniel Jackson, and Emina Torlak. A Type System for Object Models. In Foundations of Software Engineering, Newport, CA, 2004.

Digital Library

[10]

Jos B. Warmer and Anneke G. Kleppe. The Object Constraint Language: Precise Modeling with UML. Addison-Wesley, 1999.

Digital Library

[11]

J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, and L.J. Hwang. Symbolic Model Checking: 1020 States and Beyond. In Proceedings of the Fifth Annual IEEE Symposium on Logic in Computer Science, 1990.

[12]

Ken Arnold and James Gosling. The Java Programming Language. Addison-Wesley, 1996.

Digital Library

[13]

Ken L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993.

[14]

M.W. Moskewicz, C.F. Madigan, Y. Zhao, L. Zhang, and S. Malik. Chaff: Engineering an Efficient SAT Solver. In Proceedings of the 38th conference on Design automation, pages 530--535. ACM Press, 2001.

Digital Library

[15]

A. Pnueli. The Temporal Logic of Programs. In Proceedings of the 18th IEEE Symp. Foundations of Computer Science, 1977.

Digital Library

[16]

R.E. Bryant. Symbolic Boolean Manipulation with Ordered Binary-Decision Diagrams. ACM Computing Surveys, 24(3):293--318, 1992.

Digital Library

[17]

T. Ball and S.K. Rajamani. The SLAM Project: Debugging System Software via Static Analysis. In POPL '02: Proceedings of the 29th ACM Symposium on the Principles of Programming Languages, New York, NY, USA, 2002. ACM Press.

Digital Library

[18]

W. Visser, K. Havelund, G. Brat, and S. Park. Model Checking Programs. In ASE '2000: 15th IEEE International Conference on Automated Software Engineering, pages 3--11, 2000.

Digital Library

Cited By

Macedo NBrunel JChemouil DCunha A(2022)Pardinus: A Temporal Relational Model FinderJournal of Automated Reasoning10.1007/s10817-022-09642-266:4(861-904)Online publication date: 12-Sep-2022
https://doi.org/10.1007/s10817-022-09642-2
Serna JDay NEsmaeilsabzali S(2022)Dash: declarative behavioural modelling in Alloy with control state hierarchySoftware and Systems Modeling10.1007/s10270-022-01012-122:2(733-749)Online publication date: 6-Aug-2022
https://doi.org/10.1007/s10270-022-01012-1
Farheen SDay NVakili AAbbassi A(2020)Transitive-closure-based model checking (TCMC) in AlloySoftware and Systems Modeling10.1007/s10270-019-00763-8Online publication date: 3-Jan-2020
https://doi.org/10.1007/s10270-019-00763-8
Show More Cited By

Index Terms

Symbolic model checking of declarative relational models
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

Efficient software model checking of soundness of type systems

This paper presents novel techniques for checking the soundness of a type system automatically using a software model checker. Our idea is to systematically generate every type correct intermediate program state (within some finite bounds), execute the ...
Race checking by context inference
PLDI '04

Software model checking has been successful for sequential programs, where predicate abstraction offers suitable models, and counterexample-guided abstraction refinement permits the automatic inference of models. When checking concurrent programs, we ...
Symbolic assume-guarantee reasoning through BDD learning
ICSE 2014: Proceedings of the 36th International Conference on Software Engineering

Both symbolic model checking and assume-guarantee reasoning aim to circumvent the state explosion problem. Symbolic model checking explores many states simultaneously and reports numerous erroneous traces. Automated assume-guarantee reasoning, on the ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

ICSE '06: Proceedings of the 28th international conference on Software engineering

May 2006

1110 pages

ISBN:1595933751

DOI:10.1145/1134285

General Chair:
Leon J. Osterweil
University of Massachusetts, USA
,
Program Chairs:
Dieter Rombach
TU Kaiserslautern, Germany
,
Mary Lou Soffa
University of Virginia, USA

Copyright © 2006 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: 28 May 2006

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Conference

ICSE06

Sponsor:

ICSE06: International Conference on Software Engineering

May 20 - 28, 2006

Shanghai, China

Acceptance Rates

Overall Acceptance Rate 276 of 1,856 submissions, 15%

Upcoming Conference

ICSE 2025

2025 IEEE/ACM 46th International Conference on Software Engineering

April 26 - May 3, 2025

Ottawa , ON , Canada

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

19
Total Citations
View Citations
448
Total Downloads

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

Reflects downloads up to 14 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Macedo NBrunel JChemouil DCunha A(2022)Pardinus: A Temporal Relational Model FinderJournal of Automated Reasoning10.1007/s10817-022-09642-266:4(861-904)Online publication date: 12-Sep-2022
https://doi.org/10.1007/s10817-022-09642-2
Serna JDay NEsmaeilsabzali S(2022)Dash: declarative behavioural modelling in Alloy with control state hierarchySoftware and Systems Modeling10.1007/s10270-022-01012-122:2(733-749)Online publication date: 6-Aug-2022
https://doi.org/10.1007/s10270-022-01012-1
Farheen SDay NVakili AAbbassi A(2020)Transitive-closure-based model checking (TCMC) in AlloySoftware and Systems Modeling10.1007/s10270-019-00763-8Online publication date: 3-Jan-2020
https://doi.org/10.1007/s10270-019-00763-8
Daszczuk WDaszczuk W(2019)Related Work on Deadlock and Termination Detection TechniquesIntegrated Model of Distributed Systems10.1007/978-3-030-12835-7_2(17-29)Online publication date: 17-Mar-2019
https://doi.org/10.1007/978-3-030-12835-7_2
Abbassi ABandali ADay NSerna J(2018)A Comparison of the Declarative Modelling Languages B, Dash, and TLA+2018 IEEE 8th International Model-Driven Requirements Engineering Workshop (MoDRE)10.1109/MoDRE.2018.00008(11-20)Online publication date: Aug-2018
https://doi.org/10.1109/MoDRE.2018.00008
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
Serna JDay NFarheen S(2017)DASH: A New Language for Declarative Behavioural Requirements with Control State Hierarchy2017 IEEE 25th International Requirements Engineering Conference Workshops (REW)10.1109/REW.2017.70(64-68)Online publication date: Sep-2017
https://doi.org/10.1109/REW.2017.70
Macedo NBrunel JChemouil DCunha AKuperberg DZimmermann TCleland-Huang JSu Z(2016)Lightweight specification and analysis of dynamic systems with rich configurationsProceedings of the 2016 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering10.1145/2950290.2950318(373-383)Online publication date: 1-Nov-2016
https://dl.acm.org/doi/10.1145/2950290.2950318
Daszczuk W(2016)Communication and Resource Deadlock Analysis Using IMDS Formalism and Model CheckingThe Computer Journal10.1093/comjnl/bxw099Online publication date: 20-Dec-2016
https://doi.org/10.1093/comjnl/bxw099
Rosner NBengolea VPonzio PKhalek SAguirre NFrias MKhurshid S(2014)Bounded exhaustive test input generation from hybrid invariantsACM SIGPLAN Notices10.1145/2714064.266023249:10(655-674)Online publication date: 15-Oct-2014
https://dl.acm.org/doi/10.1145/2714064.2660232
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