More Web Proxy on the site http://driver.im/

research-article

Public Access

Efficient generation of inductive validity cores for safety properties

Authors:

Elaheh Ghassabani,

Michael W. WhalenAuthors Info & Claims

FSE 2016: Proceedings of the 2016 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering

Pages 314 - 325

https://doi.org/10.1145/2950290.2950346

Published: 01 November 2016 Publication History

Abstract

Symbolic model checkers can construct proofs of properties over very complex models. However, the results reported by the tool when a proof succeeds do not generally provide much insight to the user. It is often useful for users to have traceability information related to the proof: which portions of the model were necessary to construct it. This traceability information can be used to diagnose a variety of modeling problems such as overconstrained axioms and underconstrained properties, and can also be used to measure completeness of a set of requirements over a model. In this paper, we present a new algorithm to efficiently compute the em inductive validity core (IVC) within a model necessary for inductive proofs of safety properties for sequential systems. The algorithm is based on the UNSAT core support built into current SMT solvers and a novel encoding of the inductive problem to try to generate a minimal inductive validity core. We prove our algorithm is correct, and describe its implementation in the JKind model checker for Lustre models. We then present an experiment in which we benchmark the algorithm in terms of speed, diversity of produced cores, and minimality, with promising results.

References

[1]

JKind. http://loonwerks.com/tools/jkind.html.

[2]

Set of Support. https://github.com/elaghs/Working/tree/ master/support/experiments.

[3]

H. Agrawal and J. R. Horgan. Dynamic program slicing. SIGPLAN Not., 25(6):246–256, June 1990.

Digital Library

[4]

J. Backes, D. Cofer, S. Miller, and M. W. Whalen. Requirements analysis of a quad-redundant flight control system. In K. Havelund, G. Holzmann, and R. Joshi, editors, NASA Formal Methods, volume 9058 of Lecture Notes in Computer Science, pages 82–96. Springer International Publishing, 2015.

[5]

I. Beer, S. Ben-David, C. Eisner, and Y. Rodeh. Efficient detection of vacuity in ACTL formulas. In 9th International Conference on Computer Aided Verification (CAV’97), pages 279–290, Berlin, Heidelberg, 1997. Springer Berlin Heidelberg.

Digital Library

[6]

A. Belov, M. Janota, I. Lynce, and J. Marques-Silva. On computing minimal equivalent subformulas. In Principles and Practice of Constraint Programming, pages 158–174. Springer, 2012.

[7]

A. Belov, I. Lynce, and J. Marques-Silva. Towards efficient MUS extraction. AI Communications, 25(2):97–116, Apr. 2012.

Digital Library

[8]

S. Ben-David and O. Kupferman. A framework for ranking vacuity results. In Automated Technology for Verification and Analysis - 11th International Symposium, ATVA 2013, Hanoi, Vietnam, October 15-18, 2013. Proceedings, pages 148–162, 2013.

[9]

H. Chockler, O. Kupferman, and M. Vardi. Coverage metrics for formal verification. Correct hardware design and verification methods, pages 111–125, 2003.

[10]

H. Chockler and O. Strichman. Easier and more informative vacuity checks. In Proceedings of the 5th IEEE/ACM International Conference on Formal Methods and Models for Codesign, MEMOCODE ’07, pages 189–198, Washington, DC, USA, 2007. IEEE Computer Society.

Digital Library

[11]

H. Chockler and O. Strichman. Before and after vacuity. Formal Methods in System Design, 34(1):37–58, 2008.

Digital Library

[12]

J. Christ, J. Hoenicke, and A. Nutz. Smtinterpol: An interpolating smt solver. In Proceedings of the 19th International Conference on Model Checking Software, SPIN’12, pages 248–254, Berlin, Heidelberg, 2012. Springer-Verlag.

Digital Library

[13]

A. Cimatti, A. Griggio, B. J. Schaafsma, and R. Sebastiani. The mathsat5 smt solver. In Proceedings of the 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS’13, pages 93–107, Berlin, Heidelberg, 2013. Springer-Verlag.

Digital Library

[14]

A. Cimatti, A. Griggio, and R. Sebastiani. A simple and flexible way of computing small unsatisfiable cores in sat modulo theories. In Proceedings of the 10th International Conference on Theory and Applications of Satisfiability Testing, SAT’07, pages 334–339, Berlin, Heidelberg, 2007. Springer-Verlag.

Digital Library

[15]

L. De Moura and N. Bjørner. Z3: An efficient SMT solver. In Tools and Algorithms for the Construction and Analysis of Systems, pages 337–340. Springer, 2008.

Digital Library

[16]

B. Dutertre and L. D. Moura. The YICES SMT solver. Technical report, SRI, 2006.

[17]

N. Een, A. Mishchenko, and R. Brayton. Efficient implementation of property directed reachability. In Proceedings of the International Conference on Formal Methods in Computer-Aided Design, FMCAD ’11, pages 125–134, Austin, TX, 2011. FMCAD Inc.

Digital Library

[18]

F. Gaucher. Slicing lustre programs. Technical report, VERIMAG, Grenoble, February 2003.

[19]

A. Gupta, M. Ganai, Z. Yang, and P. Ashar. Iterative abstraction using sat-based bmc with proof analysis. In Proceedings of the 2003 IEEE/ACM international conference on Computer-aided design, page 416. IEEE Computer Society, 2003.

Digital Library

[20]

A. Gurfinkel and M. Chechik. Robust vacuity for branching temporal logic. ACM Trans. Comput. Logic, 13(1):1:1–1:32, Jan. 2012.

Digital Library

[21]

G. Hagen and C. Tinelli. Scaling up the formal verification of lustre programs with smt-based techniques. In Formal Methods in Computer-Aided Design, 2008. FMCAD ’08, pages 1–9, Nov 2008.

Digital Library

[22]

N. Halbwachs, P. Caspi, P. Raymond, and D. Pilaud. The Synchronous Dataflow Programming Language Lustre. Proceedings of the IEEE, 79(9):1305–1320, September 1991.

[23]

A. Ivrii, A. Gurfinkel, and A. Belov. Small inductive safe invariants. In Formal Methods in Computer-Aided Design, FMCAD 2014, Lausanne, Switzerland, 2014, pages 115–122, October 2014.

Digital Library

[24]

T. Kahsai, Y. Ge, and C. Tinelli. Instantiation-based invariant discovery. In NASA Formal Methods - Third International Symposium, NFM 2011, Pasadena, CA, USA, April 18-20, 2011. Proceedings, pages 192–206, 2011.

Digital Library

[25]

E. Keenan, A. Czauderna, G. Leach, J. Cleland-Huang, Y. Shin, E. Moritz, M. Gethers, D. Poshyvanyk, J. Maletic, J. Huffman Hayes, A. Dekhtyar, D. Manukian, S. Hossein, and D. Hearn. Tracelab: An experimental workbench for equipping researchers to innovate, synthesize, and comparatively evaluate traceability solutions. In Proceedings of the 34th International Conference on Software Engineering, ICSE ’12, pages 1375–1378, Piscataway, NJ, USA, 2012. IEEE Press.

Digital Library

[26]

O. Kupferman. Sanity checks in formal verification. In Proceedings of the 17th International Conference on Concurrency Theory, CONCUR’06, pages 37–51, Berlin, Heidelberg, 2006. Springer-Verlag.

Digital Library

[27]

O. Kupferman, W. Li, and S. Seshia. A theory of mutations with applications to vacuity, coverage, and fault tolerance. In Proceedings of the 2008 Int’l Conf. on Formal Methods in Computer-Aided Design, page 25, 2008.

Digital Library

[28]

O. Kupferman and M. Y. Vardi. Vacuity detection in temporal model checking. Journal on Software Tools for Technology Transfer, 4(2), February 2003.

[29]

H. F. Li, J. Rilling, and D. Goswami. Granularity-driven dynamic predicate slicing algorithms for message passing systems. Automated Software Engineering, 11(1):63–89, 2004.

Digital Library

[30]

J. Marques-Silva. Minimal unsatisfiability: Models, algorithms and applications. In Multiple-Valued Logic (ISMVL), 2010 40th IEEE International Symposium on, pages 9–14. IEEE, 2010.

Digital Library

[31]

MathWorks Inc. Simulink Design Verifier. http://www.mathworks.com/products/sldesignverifier, 2015.

[32]

MathWorks Inc. Simulink Requirements Traceability. http://www.mathworks.com/discovery/requirementstraceability.html, 2016.

[33]

K. L. McMillan. A methodology for hardware verification using compositional model checking. Technical Report 1999-01, Cadence Berkeley Labs, Berkeley, CA 94704, 1999.

[34]

K. L. McMillan and N. Amla. Automatic abstraction without counterexamples. In Tools and Algorithms for the Construction and Analysis of Systems, pages 2–17. Springer, 2003.

Digital Library

[35]

S. P. Miller, M. W. Whalen, and D. D. Cofer. Software model checking takes off. Commun. ACM, 53(2):58–64, 2010.

Digital Library

[36]

Requirements for Safety Related Software in Defence Equipment, Issue 2. UK Ministry of Defence, 1997.

[37]

A. Murugesan, M. W. Whalen, E. Ghassabani, and M. P. Heimdahl. Complete traceability for requirements in satisfaction arguments. In Proceedings of the International Conference on Requirements Engineering (RE@Next! Track). IEEE, September 2016.

[38]

A. Murugesan, M. W. Whalen, S. Rayadurgam, and M. P. Heimdahl. Compositional verification of a medical device system. In ACM Int’l Conf. on High Integrity Language Technology (HILT) 2013. ACM, November 2013.

Digital Library

[39]

A. Murugesan, M. W. Whalen, N. Rungta, O. Tkachuk, S. Person, M. P. Heimdahl, and D. You. Are we there yet? Determining the adequacy of formalized requirements and test suites. In NASA Formal Methods, pages 279–294. Springer, 2015.

[40]

A. Nadel. Boosting minimal unsatisfiable core extraction. In Formal Methods in Computer-Aided Design (FMCAD), 2010, pages 221–229. IEEE, 2010.

Digital Library

[41]

RTCA/DO-178C. Software considerations in airborne systems and equipment certification.

[42]

V. Ryvchin and O. Strichman. Faster extraction of high-level minimal unsatisfiable cores. In Theory and Applications of Satisfiability Testing-SAT 2011, pages 174–187. Springer, 2011.

Digital Library

[43]

D. Schuler and A. Zeller. Assessing oracle quality with checked coverage. In Proceedings of the Fourth IEEE Int’l Conf. on Software Testing, Verification and Validation, pages 90–99, 2011.

Digital Library

[44]

M. Sheeran, S. Singh, and G. Stålmarck. Checking safety properties using induction and a SAT-solver. In FMCAD, pages 108–125, 2000.

Digital Library

[45]

F. Tip. A survey of program slicing techniques. Journal of Programming Languages, 3:121–189, 1995.

[46]

E. Torlak, F. S.-H. Chang, and D. Jackson. Finding minimal unsatisfiable cores of declarative specifications. In Proceedings of the 15th International Symposium on Formal Methods, FM ’08, pages 326–341, Berlin, Heidelberg, 2008. Springer-Verlag.

Digital Library

[47]

M. Weiser. Program slicing. In Proceedings of the 5th International Conference on Software Engineering, ICSE ’81, pages 439–449, Piscataway, NJ, USA, 1981. IEEE Press.

Digital Library

[48]

M. Whalen, G. Gay, D. You, M. Heimdahl, and M. Staats. Observable modified condition/decision coverage. In Proceedings of the 2013 Int’l Conf. on Software Engineering. ACM, May 2013.

Digital Library

[49]

D. You, S. Rayadurgam, M. Whalen, and M. Heimdahl. Efficient observability-based test generation by dynamic symbolic execution. In 26th International Symposium on Software Reliability Engineering (ISSRE 2015), November 2015.

Digital Library

[50]

L. Zhang and S. Malik. Extracting small unsatisfiable cores from unsatisfiable boolean formula. In 6th International Conference on Theory and Applications of Satisfiability Testing: SAT 2003, May 2003.

Cited By

Larraz DViswanathan ATinelli CLaurent M(2023)Beyond model checking of idealized Lustre in Kind 2ACM SIGAda Ada Letters10.1145/3591335.359133842:2(40-44)Online publication date: 5-Apr-2023
https://dl.acm.org/doi/10.1145/3591335.3591338
Larraz DTinelli C(2023)Finding Locally Smallest Cut Sets using Max-SMTACM SIGAda Ada Letters10.1145/3591335.359133742:2(32-39)Online publication date: 5-Apr-2023
https://dl.acm.org/doi/10.1145/3591335.3591337
Beyer DDangl MDietsch DHeizmann MLemberger TTautschnig M(2022)Verification WitnessesACM Transactions on Software Engineering and Methodology10.1145/347757931:4(1-69)Online publication date: 8-Sep-2022
https://dl.acm.org/doi/10.1145/3477579
Show More Cited By

Index Terms

Efficient generation of inductive validity cores for safety properties
1. Software and its engineering
  1. Software creation and management
    1. Designing software
      1. Requirements analysis
    2. Software verification and validation
      1. Formal software verification
2. Theory of computation
  1. Logic
    1. Automated reasoning
    2. Verification by model checking

Recommendations

Inductive Validity Cores
Symbolic model checkers can construct proofs of properties over highly complex models. However, the results reported by the tool when a proof succeeds do not generally provide much insight to the user. It is often useful for users to have traceability ...
Efficient generation of all minimal inductive validity cores
FMCAD '17: Proceedings of the 17th Conference on Formal Methods in Computer-Aided Design

Symbolic model checkers can construct proofs of safety properties over complex models, but when a proof succeeds, the results do not generally provide much insight to the user. Recently, proof cores (alternately, for inductive model checkers, Inductive ...
Handling loops in bounded model checking of C programs via k-induction

The first attempts to apply the k-induction method to software verification are only recent. In this paper, we present a novel proof by induction algorithm, which is built on the top of a symbolic context-bounded model checker and uses an iterative ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

FSE 2016: Proceedings of the 2016 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering

November 2016

1156 pages

ISBN:9781450342186

DOI:10.1145/2950290

General Chair:
Thomas Zimmermann
Microsoft Research, USA
,
Program Chairs:
Jane Cleland-Huang
University of Notre Dame, USA
,
Zhendong Su
University of California at Davis, USA

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

SIGSOFT: ACM Special Interest Group on Software Engineering

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 November 2016

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

Conference

FSE'16

Sponsor:

SIGSOFT

FSE'16: 24nd ACM SIGSOFT International Symposium on the Foundations of Software Engineering

November 13 - 18, 2016

WA, Seattle, USA

Acceptance Rates

Overall Acceptance Rate 17 of 128 submissions, 13%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

24
Total Citations
View Citations
504
Total Downloads

Downloads (Last 12 months)85
Downloads (Last 6 weeks)8

Reflects downloads up to 12 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Larraz DViswanathan ATinelli CLaurent M(2023)Beyond model checking of idealized Lustre in Kind 2ACM SIGAda Ada Letters10.1145/3591335.359133842:2(40-44)Online publication date: 5-Apr-2023
https://dl.acm.org/doi/10.1145/3591335.3591338
Larraz DTinelli C(2023)Finding Locally Smallest Cut Sets using Max-SMTACM SIGAda Ada Letters10.1145/3591335.359133742:2(32-39)Online publication date: 5-Apr-2023
https://dl.acm.org/doi/10.1145/3591335.3591337
Beyer DDangl MDietsch DHeizmann MLemberger TTautschnig M(2022)Verification WitnessesACM Transactions on Software Engineering and Methodology10.1145/347757931:4(1-69)Online publication date: 8-Sep-2022
https://dl.acm.org/doi/10.1145/3477579
Hobbs KDavis JWagner LFeron E(2021)Formal Specification and Analysis of Spacecraft Collision Avoidance Run Time Assurance Requirements2021 IEEE Aerospace Conference (50100)10.1109/AERO50100.2021.9438135(1-16)Online publication date: 6-Mar-2021
https://doi.org/10.1109/AERO50100.2021.9438135
Stewart DWhalen MHeimdahl MLiu JCofer D(2021)Composition of Fault ForestsComputer Safety, Reliability, and Security10.1007/978-3-030-83903-1_17(258-275)Online publication date: 25-Aug-2021
https://doi.org/10.1007/978-3-030-83903-1_17
Wagner LGacek A(2020)Automating Certification Objectives with SpeARACM SIGAda Ada Letters10.1145/3379106.337911139:1(35-49)Online publication date: 10-Jan-2020
https://dl.acm.org/doi/10.1145/3379106.3379111
Hobbs KPerez IFifarek AFeron E(2019)Formal Verification of System States for Spacecraft Automatic ManeuveringAIAA Scitech 2019 Forum10.2514/6.2019-1187Online publication date: 6-Jan-2019
https://doi.org/10.2514/6.2019-1187
Berryhill RVeneris A(2019)Chasing Minimal Inductive Validity Cores in Hardware Model Checking2019 Formal Methods in Computer Aided Design (FMCAD)10.23919/FMCAD.2019.8894268(19-27)Online publication date: Oct-2019
https://doi.org/10.23919/FMCAD.2019.8894268
Todorov VTaha SBoulanger FHernandez A(2019)Improved Invariant Generation for Industrial Software Model Checking of Time Properties2019 IEEE 19th International Conference on Software Quality, Reliability and Security (QRS)10.1109/QRS.2019.00050(334-341)Online publication date: Jul-2019
https://doi.org/10.1109/QRS.2019.00050
Groce AAhmed IJensen CMckenney PHolmes J(2018)How verified (or tested) is my code? Falsification-driven verification and testingAutomated Software Engineering10.5555/3288647.328871225:4(917-960)Online publication date: 1-Dec-2018
https://dl.acm.org/doi/10.5555/3288647.3288712
Show More Cited By

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