research-article

Avestan: a declarative modeling language based on SMT-LIB

Authors:

Amirhossein Vakili,

Nancy A. DayAuthors Info & Claims

MiSE '12: Proceedings of the 4th International Workshop on Modeling in Software Engineering

Pages 36 - 42

Published: 02 June 2012 Publication History

Abstract

Avestan is a declarative modelling language compatible with SMT-LIB. SMT-LIB is an standard input language that is supported by the state-of-the-art satisfiability modulo theory solvers (SMT solvers). The recent advances in SMT solvers have introduced them as efficient analysis tools; as a result, they are becoming more popular in the verification and certification of digital products. SMT-LIB was designed to be machine readable rather than human readable. In this paper, we present Avestan, a declarative modelling language that is intended to be analyzed by SMT solvers and readable by humans. An Avestan model is translated to an SMT-LIB model so that it can be analyzed by different SMT solvers. Avestan has relational constructs that are heavily inspired by Alloy; we added these constructs to increase the readability of an Avestan model.

References

[1]

C. Barrett, A. Stump, and C. Tinelli, The SMT-LIB Standard Version 2.0 Reference Manual, Jan. 2010. {Online}. Available: www.SMT-LIB.org

[2]

L. de Moura and N. Bjørner, "Z3: An Efficient SMT Solver," in Tools and Algorithms for the Construction and Analysis of Systems, ser. LNCS. Springer, 2008, vol. 4963, pp. 337--340.

Digital Library

[3]

C. Barrett and C. Tinelli, "CVC3," in Proceedings of the 19th international conference on Computer aided verification, ser. CAV'07. Springer-Verlag, 2007, pp. 298--302.

Digital Library

[4]

D. Jackson, "Alloy: a lightweight object modelling notation," ACM TOSEM, vol. 11, no. 2, pp. 256--290, 2002.

Digital Library

[5]

"http://www.cs.uwaterloo.ca/~avakili/projects/avestan."

[6]

M. Manzano, Introduction to many-sorted logic. John Wiley & Sons, Inc., 1993, pp. 3--86.

Digital Library

[7]

D. Jackson, Software Abstractions - Logic, Language, and Analysis. MIT Press, 2006.

Digital Library

[8]

Information Technology Z Formal Specification Notation Syntax, Type System and Semantics, International Organisation for Standardization, 2000.

[9]

J. Joyce, N. Day, and M. Donat, "S: A machine readable specification notation based on higher order logic," in 7th International Workshop on Higher Order Logic Theorem Proving and Its Applications. Valletta, Malta: Springer-Verlag, September 1994, pp. 285--299.

Digital Library

[10]

ProofPower. {Online}. Available: http://www.lemma-one.com/ProofPower/index/index.html

[11]

A. A. E. Ghazi and M. Taghdiri, "Analyzing Alloy Constraints using an SMT Solver: A Case Study," in Automated Formal Methods (AFM) workshop, 2010.

[12]

B. Dutertre and L. De Moura, "The Yices SMT Solver," Tool paper at httpyices csl sri comtoolpaper, pp. 1--5, 2006.

[13]

M. Cadoli and A. Schaerf, "Compiling problem specifications into sat," Artificial Intelligence, vol. 162, no. 12, pp. 89--120, 2005.

Digital Library

[14]

M. J. C. Gordon and T. F. Melham, Eds., Introduction to HOL: a theorem proving environment for higher order logic. Cambridge University Press, 1993.

Digital Library

[15]

E. Börger, "The ASM Method for System Design and Analysis. A Tutorial Introduction," in Frontiers of Combining Systems, ser. LNCS. Springer, 2005, vol. 3717, pp. 264--283.

Digital Library

[16]

G. Schellhorn and W. Ahrendt, "Reasoning about Abstract State Machines: The WAM Case Study," Journal of Universal Computer Science, vol. 3, no. 4, pp. 377--413, 1997.

[17]

A. Dold, "A Formal Representation of Abstract State Machines Using PVS," Universität Ulm, Verifix Technical Report Ulm/6.2, Jul. 1998.

[18]

G. Del Castillo and K. Winter, "Model Checking Support for the ASM High-Level Language," in Tools and Algorithms for the Construction and Analysis of Systems, ser. LNCS. Springer, 2000, vol. 1785, pp. 331--346.

Digital Library

[19]

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

Digital Library

[20]

M. Leuschel and M. Butler, "ProB: A Model Checker for B," in FME 2003: Formal Methods, ser. LNCS. Springer, 2003, vol. 2805, pp. 855--874.

[21]

E. Clarke, O. Grumberg, and D. A. Peled, Model Checking. MIT Press, 1999.

Digital Library

[22]

D. Marinov, S. Khurshid, S. Bugrara, L. Zhang, and M. Rinard, "Optimizations for Compiling Declarative Models into Boolean Formulas," in Theory and Applications of Satisfiability Testing, ser. LNCS. Springer, 2005, vol. 3569.

Digital Library

[23]

B. Selic, "From Model-Driven Development to Model-Driven Engineering," in ECRTS. IEEE Computer Society, 2007.

Digital Library

[24]

J. Wielemaker, "SWI-Prolog 5.3 Reference Manual," 2004.

Cited By

Vakili ADay NCheung SOrso AStorey M(2014)Verifying CTL-live properties of infinite state models using an SMT solverProceedings of the 22nd ACM SIGSOFT International Symposium on Foundations of Software Engineering10.1145/2635868.2635911(213-223)Online publication date: 11-Nov-2014
https://dl.acm.org/doi/10.1145/2635868.2635911

Recommendations

Model generation for quantified formulas with application to test data generation

We present a new model generation approach and technique for solving first-order logic (FOL) formulas with quantifiers in unbounded domains. Model generation is important, e.g., for test data generation based on test data constraints and for ...
Model checking memoryful linear-time logics over one-counter automata

We study complexity of the model-checking problems for LTL with registers (also known as freeze LTL and written LTL"^@7) and for first-order logic with data equality tests (written FO^(~,<,+1)) over one-counter automata. We consider several classes of ...
Evaluation of SMT solvers in abstraction-based software model checking
LADC '22: Proceedings of the 11th Latin-American Symposium on Dependable Computing

The verification of safety-critical software systems is an algorithmically complex task, which often utilizes SMT (Satisfiability Modulo Theory) solvers for computing abstractions and refinements. It follows that the performance of SMT solvers impacts ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

MiSE '12: Proceedings of the 4th International Workshop on Modeling in Software Engineering

June 2012

102 pages

ISBN:9781467317573

Conference Chairs:
Joanne Atlee
University of Waterloo, Canada
,
Robert Baillargeon
Sodius
,
Robert France
Colorado State University
,
Geri Georg
Colorado State University
,
Ana Moreira
Universidade Nova Lisboa, Portugal
,
Bernhard Rumpe
RWTH Aachen University, Germany
,
Steffen Zschaler
King's College London, UK

Sponsors

SIGSOFT: ACM Special Interest Group on Software Engineering
University of Zurich: University of Zurich
IEEE CS

Publisher

IEEE Press

Publication History

Published: 02 June 2012

Check for updates

Author Tags

Qualifiers

Research-article

Conference

ICSE '12

Sponsor:

SIGSOFT
University of Zurich

ICSE '12: 34th International Conference on Software Engineering

June 2 - 3, 2012

Zurich, Switzerland

Acceptance Rates

Overall Acceptance Rate 13 of 30 submissions, 43%

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

1
Total Citations
View Citations
35
Total Downloads

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

Reflects downloads up to 20 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Vakili ADay NCheung SOrso AStorey M(2014)Verifying CTL-live properties of infinite state models using an SMT solverProceedings of the 22nd ACM SIGSOFT International Symposium on Foundations of Software Engineering10.1145/2635868.2635911(213-223)Online publication date: 11-Nov-2014
https://dl.acm.org/doi/10.1145/2635868.2635911

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