short-paper

SIMPAL: a compositional reasoning framework for imperative programs

Authors:

Lucas Wagner,

David Greve,

Andrew GacekAuthors Info & Claims

SPIN 2017: Proceedings of the 24th ACM SIGSOFT International SPIN Symposium on Model Checking of Software

Pages 90 - 93

https://doi.org/10.1145/3092282.3092290

Published: 13 July 2017 Publication History

Get Access

Abstract

The Static IMPerative AnaLyzer (SIMPAL) is a tool for performing compositional reasoning over software programs that utilize preexisting software components. SIMPAL features a specification language, called Limp, for modeling programs that utilize preexisting components. Limp is an extension of the Lustre synchronous data flow language. Limp extends Lustre by introducing control flow elements, global variables, and syntax specifying preconditions, postconditions, and global variable interactions of preexisting components.

SIMPAL translates Limp programs to an equivalent Lustre representation which can be passed to the JKind model checking tool to perform assume-guarantee reasoning, reachability, and viability analyses. The feedback from these analyses can be used to refine the program to ensure the software functions as intended.

References

[1]

Roberto Cavada, Alessandro Cimatti, Michele Dorigatti, Alberto Griggio, Alessandro Mariotti, Andrea Micheli, Sergio Mover, Marco Roveri, and Stefano Tonetta. 2014. The nuXmv Symbolic Model Checker. In Computer Aided Verification - 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014. Proceedings (Lecture Notes in Computer Science), Armin Biere and Roderick Bloem (Eds.), Vol. 8559. Springer, 334–342.

Digital Library

Google Scholar

[2]

Adrien Champion, Alain Mebsout, Christoph Sticksel, and Cesare Tinelli. 2016. The Kind 2 Model Checker. Springer International Publishing, Cham, 510–517.

Google Scholar

[3]

Alessandro Cimatti, Michele Dorigatti, and Stefano Tonetta. 2013. OCRA: A tool for checking the refinement of temporal contracts. In 2013 28th IEEE/ACM International Conference on Automated Software Engineering, ASE 2013, Silicon Valley, CA, USA, November 11-15, 2013, Ewen Denney, Tevfik Bultan, and Andreas Zeller (Eds.). IEEE, 702–705.

Digital Library

Google Scholar

[4]

Alessandro Cimatti, Alberto Griggio, Sergio Mover, and Stefano Tonetta. 2015. HyComp: An SMT-Based Model Checker for Hybrid Systems. In Tools and Algorithms for the Construction and Analysis of Systems - 21st International Conference, TACAS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings (Lecture Notes in Computer Science), Christel Baier and Cesare Tinelli (Eds.), Vol. 9035. Springer, 52–67.

Digital Library

Google Scholar

[5]

Edmund Clarke, Daniel Kroening, and Flavio Lerda. 2004. A Tool for Checking ANSI-C Programs. Springer Berlin Heidelberg, Berlin, Heidelberg, 168–176.

Google Scholar

[6]

Darren Cofer, Andrew Gacek, Steven Miller, Michael W. Whalen, Brian LaValley, and Lui Sha. 2012. Compositional Verification of Architectural Models. In Proceedings of the 4th International Conference on NASA Formal Methods (NFM’12). Springer-Verlag, Berlin, Heidelberg, 126–140.

Digital Library

Google Scholar

[7]

Patrick Cousot and Radhia Cousot. 1977. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages. ACM, 238–252.

Digital Library

Google Scholar

[8]

Peter H. Feiler and David P. Gluch. 2012. Model-Based Engineering with AADL: An Introduction to the SAE Architecture Analysis & Design Language (1st ed.). Addison-Wesley Professional.

Digital Library

Google Scholar

[9]

Andrew Gacek. 2014. The JKind model checker. (2014). http://loonwerks.com/ tools/jkind.html

Google Scholar

[10]

Susanne Graf, Roberto Passerone, and Sophie Quinton. 2014. Contract-Based Reasoning for Component Systems with Rich Interactions. Springer New York, New York, NY, 139–154.

Google Scholar

[11]

Nicholas Halbwachs, Paul Caspi, Pascal Raymond, and Daniel Pilaud. 1991. The synchronous data flow programming language LUSTRE. Proc. IEEE 79, 9 (1991), 1305–1320.

Crossref

Google Scholar

[12]

Duc Hoang, Yannick Moy, Angela Wallenburg, and Roderick Chapman. 2015. SPARK 2014 and GNATprove. Int. J. Softw. Tools Technol. Transf. 17, 6 (Nov. 2015), 695–707.

Digital Library

Google Scholar

[13]

Florent Kirchner, Nikolai Kosmatov, Virgile Prevosto, Julien Signoles, and Boris Yakobowski. 2015. Frama-C: A software analysis perspective. Formal Aspects of Computing 27, 3 (2015), 573–609.

Digital Library

Google Scholar

Cited By

View all

Cardoso RDennis LFarrell MFisher MLuckcuck M(2020)Towards Compositional Verification for Modular Robotic SystemsElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.329.2329(15-22)Online publication date: 3-Dec-2020
https://doi.org/10.4204/EPTCS.329.2
Gacek ABackes JWhalen MWagner LGhassabani E(2018)The JKind Model CheckerComputer Aided Verification10.1007/978-3-319-96142-2_3(20-27)Online publication date: 18-Jul-2018
https://doi.org/10.1007/978-3-319-96142-2_3

Index Terms

SIMPAL: a compositional reasoning framework for imperative programs
1. Theory of computation
  1. Logic

Recommendations

Towards a compositional SPIN
SPIN'06: Proceedings of the 13th international conference on Model Checking Software

This paper discusses our initial experience with introducing automated assume-guarantee verification based on learning in the SPIN tool. We believe that compositional verification techniques such as assume-guarantee reasoning could complement the state-...
Filter-based model checking of partial systems
SIGSOFT '98/FSE-6: Proceedings of the 6th ACM SIGSOFT international symposium on Foundations of software engineering

Recent years have seen dramatic growth in the application of model checking techniques to the validation and verification of correctness properties of hardware, and more recently software, systems. Most of this work has been aimed at reasoning about ...
Compositional Abstraction Refinement for Timed Systems
TASE '10: Proceedings of the 2010 4th IEEE International Symposium on Theoretical Aspects of Software Engineering

Model checking suffers from the state explosion problem. Compositional abstraction and abstraction refinement have been investigated in many areas to address this problem. This paper considers the compositional model checking for timed systems. We ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

SPIN 2017: Proceedings of the 24th ACM SIGSOFT International SPIN Symposium on Model Checking of Software

July 2017

199 pages

ISBN:9781450350778

DOI:10.1145/3092282

Program Chairs:
Hakan Erdogmus
Carnegie Mellon University, USA
,
Klaus Havelund
NASA, USA / Jet Propulsion Laboratory, USA

© 2017 Association for Computing Machinery. ACM acknowledges that this contribution was authored or co-authored by an employee, contractor or affiliate of the United States government. As such, the United States Government retains a nonexclusive, royalty-free right to publish or reproduce this article, or to allow others to do so, for Government purposes only.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 13 July 2017

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Short-paper

Conference

ISSTA '17

Sponsor:

SIGSOFT

ISSTA '17: International Symposium on Software Testing and Analysis

July 13 - 14, 2017

CA, Santa Barbara, USA

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

2
Total Citations
View Citations
64
Total Downloads

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

Reflects downloads up to 01 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

View all

Cardoso RDennis LFarrell MFisher MLuckcuck M(2020)Towards Compositional Verification for Modular Robotic SystemsElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.329.2329(15-22)Online publication date: 3-Dec-2020
https://doi.org/10.4204/EPTCS.329.2
Gacek ABackes JWhalen MWagner LGhassabani E(2018)The JKind Model CheckerComputer Aided Verification10.1007/978-3-319-96142-2_3(20-27)Online publication date: 18-Jul-2018
https://doi.org/10.1007/978-3-319-96142-2_3

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Cited By

Index Terms

Recommendations

Towards a compositional SPIN

Filter-based model checking of partial systems

Compositional Abstraction Refinement for Timed Systems