Inductive Validity Cores
Pages 279 - 299
Abstract
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 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, measure <italic>completeness</italic> of a set of requirements over a model, and assist with <italic>design optimization</italic> given a set of requirements for an existing or synthesized implementation. In this paper, we present a comprehensive treatment of a suite of algorithms to compute <italic>inductive validity cores</italic> (IVCs), minimal sets of model elements necessary to construct inductive proofs of safety properties for sequential systems. The algorithms are based on the UNSAT core support built into current SMT solvers and novel encodings of the inductive problem to generate approximate and guaranteed minimal inductive validity cores as well as <italic>all</italic> inductive validity cores. We demonstrate that our algorithms are correct, describe their implementation in the JKind model checker for Lustre models, and present several use cases for the algorithms. We then present a substantial experiment in which we benchmark the efficiency and efficacy of the algorithms.
References
[1]
N. Een, A. Mishchenko, and R. Brayton, “Efficient implementation of property directed reachability,” in Proc. Int. Conf. Formal Methods Comput.-Aided Des., 2011, pp. 125–134.
[2]
M. Sheeran, S. Singh, and G. Stålmarck, “Checking safety properties using induction and a sat-solver,” in Proc. Int. Conf. Formal Methods Comput.-Aided Des., 2000, pp. 127–144.
[3]
K. Claessen and N. Srensson, “A liveness checking algorithm that counts,” in Proc. Formal Methods Comput.-Aided Des., 2012, pp. 52–59.
[4]
A. Murugesan, M. W. Whalen, S. Rayadurgam, and M. P. Heimdahl, “Compositional verification of a medical device system,” in Proc. ACM Int. Conf. High Integrity Lang. Technol., Nov. 2013.
[5]
K. L. McMillan, “A methodology for hardware verification using compositional model checking,” Cadence Berkeley Labs, Berkeley, CA, USA, Tech. Rep., 1999.
[6]
S. P. Miller, M. W. Whalen, and D. D. Cofer, “Software model checking takes off,” Commun. ACM, vol. 53, no. 2, pp. 58–64, 2010.
[7]
M. Whalen, G. Gay, D. You, M. Heimdahl, and M. Staats, “Observable modified condition/decision coverage,” in Proc. Int. Conf. Softw. Eng., May 2013, pp. 102–111.
[8]
D. You, S. Rayadurgam, M. Whalen, and M. Heimdahl, “Efficient observability-based test generation by dynamic symbolic execution,” in Proc. 26th Int. Symp. Softw. Rel. Eng., Nov. 2015, pp. 228–238.
[9]
O. Kupferman and M. Y. Vardi, “Vacuity detection in temporal model checking,” Int. J. Softw. Tools Technol. Transfer, vol. 4, no. 2, pp. 224–233, 2003.
[10]
M. Whalen, D. Cofer, S. Miller, B. H. Krogh, and W. Storm, “Integration of formal analysis into a model-based software development process,” in Proc. Int. Workshop Formal Methods Ind. Critical Syst., 2007, pp. 68–84.
[11]
L. Pike, “A note on inconsistent axioms in rushby's “systematic formal verification for fault-tolerant time-triggered algorithms”,” IEEE Trans. Softw. Eng., vol. 32, no. 5, pp. 347–348, May 2006.
[12]
L. Zhang and S. Malik, “Extracting small unsatisfiable cores from unsatisfiable boolean formula,” in SAT'03 vol. LNCS 2919, 2003.
[13]
E. Torlak, F. S.-H. Chang, and D. Jackson, “Finding minimal unsatisfiable cores of declarative specifications,” in Proc. 15th Int. Symp. Formal Methods, 2008, pp. 326–341. [Online]. Available: https://doi.org/10.1007/978-3-540-68237-0_23
[14]
Cadence JasperGold Formal Verification Platform. (2017). [Online]. Available: https://www.cadence.com/
[15]
RTCA/DO-178C, “Software considerations in airborne systems and equipment certification.” Washington, DC, Dec. 2011.
[16]
D. S. 00-55 Requirements for Safety Related Software in Defence Equipment, Issue 2. UK Ministry of Defence, 1997.
[17]
MathWorks Inc. Simulink Requirements Traceability, 2016. [Online]. Available: http://www.mathworks.com/discovery/requirements-traceability.html
[18]
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 Proc. 34th Int. Conf. Softw. Eng., 2012, pp. 1375–1378. [Online]. Available: http://dl.acm.org/citation.cfm?id=2337223.2337422
[19]
H. Chockler, O. Kupferman, and M. Vardi, “Coverage metrics for formal verification,” Correct Hardware Des. Verification Methods, vol. LNCS 2860, pp. 111–125, 2003.
[20]
O. Kupferman, W. Li, and S. Seshia, “A theory of mutations with applications to vacuity, coverage, and fault tolerance,” in Proc. Int. Conf. Formal Methods Comput.-Aided Des., 2008, Art. no.
[21]
MathWorks Inc. Simulink Design Verifier, 2015. [Online]. Available: http://www.mathworks.com/products/sldesignverifier
[22]
E. Ghassabani, A. Gacek, and M. W. Whalen, “Efficient generation of inductive validity cores for safety properties,” in Proc. 24th ACM SIGSOFT Int. Symp. Found. Softw. Eng., 2016, pp. 314–325.
[23]
A. Murugesan, M. W. Whalen, E. Ghassabani, and M. P. Heimdahl, “Complete traceability for requirements in satisfaction arguments,” in Proc. IEEE 24th Int. Requirements Eng. Conf., 2016, pp. 359–364.
[24]
E. Ghassabani, A. Gacek, M. W. Whalen, M. Heimdahl, and W. Lucas, “Proof-based coverage metrics for formal verification,” in Proc. 32nd IEEE/ACM Int. Conf. Autom. Softw. Eng., 2017, pp. 194–199.
[25]
E. Ghassabani, A. Gacek, and M. W. Whalen, “Efficient generation of all minimal inductive validity cores,” in Proc. Int. Conf. Formal Methods Comput.-Aided Des., 2017, pp. 31–38.
[26]
A. Mebsout and C. Tinelli, “Proof certificates for smt-based model checkers for infinite-state systems,” in Proc. 16th Conf. Formal Methods Comput.-Aided Des., 2016, pp. 117–124.
[27]
M. P. E. Heimdahl, Y. Choi, and M. Whalen, “Deviation analysis through model checking,” in Proc. 17th IEEE Int. Conf. Autom. Softw. Eng., 2002, pp. 37–46. [Online]. Available: http://dl.acm.org/citation.cfm?id=786769.787040
[28]
A. Gacek, J. Backes, M. Whalen, L. Wagner, and E. Ghassabani, “The JKind model checker,” in Proc. Int. Conf. Comput. Aided Verification, 2018, pp. 20–27.
[29]
M. H. Liffiton, A. Previti, A. Malik, and J. Marques-Silva, “Fast, flexible MUS enumeration,” Constraints, vol. 21, no. 2, pp. 223–250, 2016.
[30]
J. Davies and F. Bacchus, “Solving MAXSAT by solving a sequence of simpler sat instances,” in Proc. Int. Conf. Principles Practice Constraint Program., 2011, pp. 225–239.
[31]
A. Morgado, F. Heras, M. Liffiton, J. Planes, and J. Marques-Silva, “Iterative and core-guided MaxSAT solving: A survey and assessment,” Constraints, vol. 18, no. 4, pp. 478–534, 2013.
[32]
N. Halbwachs, P. Caspi, P. Raymond, and D. Pilaud, “The synchronous data flow programming language lustre,” Proc. IEEE, vol. 79, no. 9, pp. 1305–1320, Sep. 1991.
[33]
T. Kahsai, Y. Ge, and C. Tinelli, “Instantiation-based invariant discovery,” in Proc. 3rd Int. Symp. NASA Formal Methods, 2011, pp. 192–206.
[34]
L. De Moura and N. Bjørner, “Z3: An efficient SMT solver,” in Proc. Int. Conf. Tools Algorithms Construction Anal. Syst., 2008, pp. 337–340.
[35]
B. Dutertre and L. De Moura, “The YICES SMT solver,” Tool Paper, vol. 2, no. 2, pp. 1–2, 2006, http://yices. csl. sri. com/tool-paper. pdf
[36]
A. Cimatti, et al., “The MathSAT5 SMT solver,” in Proc. 19th Int. Conf. Tools Algorithms Construction Anal. Syst., 2013, pp. 93–107.
[37]
J. Christ, J. Hoenicke, and A. Nutz, “SMTInterpol: An interpolating SMT solver,” in Proc. Int. SPIN Workshop Model Checking Softw., 2012, pp. 248–254.
[38]
E. Ghassabani, “Inductive validity cores,” Ph.D. dissertation, Comput. Sci. Dept., University of Minnesota- Twin Cities, Minneapolis, MN, USA, Oct. 2018.
[39]
D. D. Cofer, A. Gacek, S. P. Miller, M. W. Whalen, B. LaValley, and L. Sha, “Compositional verification of architectural models,” in Proc. 4th NASA Formal Methods Symp., Apr. 2012, pp. 126–140.
[40]
J. Backes, D. Cofer, S. Miller, and M. W. Whalen, “Requirements analysis of a quad-redundant flight control system,” in NASA Formal Methods, vol. 9058. New York, NY, USA: Springer, 2015, pp. 82–96.
[41]
G. Hagen and C. Tinelli, “Scaling up the formal verification of lustre programs with smt-based techniques,” in Proc. Int. Conf. Formal Methods Comput.-Aided Des., 2008, Art. no.
[42]
J. Backes, D. Cofer, S. Miller, and M. W. Whalen, “Requirements analysis of a quad-redundant flight control system,” in NASA Formal Methods, K. Havelund, G. Holzmann, and R. Joshi, Eds., vol. 9058. New York, NY, USA: Springer International Publishing, 2015, pp. 82–96. [Online]. Available: https://doi.org/10.1007/978-3-319-17524-9_7
[43]
IVCs repository. [Online]. Available: https://github.com/elaghs/Working/tree/master/TSE/experiments
[44]
F. Tip, “A survey of program slicing techniques,” J. Program. Lang., vol. 3, pp. 121–189, 1995.
[45]
F. Gaucher, “Slicing lustre programs,” VERIMAG, Grenoble, France, Tech. Rep., Feb. 2003.
[46]
O. C. Z. Gotel and C. W. Finkelstein, “An analysis of the requirements traceability problem,” in Proc. 1st Int. Conf. Requirements Eng., Apr. 1994, pp. 94–101.
[47]
O. Gotel, J. Cleland-Huang, J. H. Hayes, A. Zisman, A. Egyed, P. Grünbacher, A. Dekhtyar, G. Antoniol, J. Maletic, and P. Mäder, “Traceability fundamentals,” in Software and Systems Traceability. New York, NY, USA: Springer, 2012, pp. 3–22.
[48]
P. Zave and M. Jackson, “Four dark corners of requirements engineering,” ACM Trans. Softw. Eng. Meth., vol. 6, no. 1, pp. 1–30, 1997.
[49]
J. H. Hayes, A. Dekhtyar, and J. Osborne, “Improving requirements tracing via information retrieval,” in Proc. 11th IEEE Int. Requirements Eng. Conf., 2003, pp. 138–147.
[50]
A. Egyed and P. Grunbacher, “Automating requirements traceability: Beyond the record & replay paradigm,” in Proc. 17th IEEE Int. Conf. Autom. Softw. Eng., 2002, pp. 163–171.
[51]
J. Cleland-Huang, B. Berenbach, S. Clark, R. Settimi, and E. Romanova, “Best practices for automated traceability,” Comput., vol. 40, no. 6, pp. 27–35, Jun. 2007.
[52]
J. Hammond, R. Rawlings, and A. Hall, “Will it work? [requirements engineering],” in Proc. 5th IEEE Int. Symp. Requirements Eng., 2001, pp. 102–109.
[53]
Esterel-Technologies, “SCADE Suite product description,” 2018. [Online]. Available: http://www.esterel-technologies.com/products/scade-suite/
[54]
imulink - simulation and model-based design. [Online]. Available: http://www.mathworks.com/products/simulink/
[55]
H. Bourbouh, P.-L. Garoche, C. Garion, A. Gurfinkel, T. Kahsai, and X. Thirioux, “Automated analysis of stateflow models,” in Proc. 21st Int. Conf. Logic Program. Artif. Intell. Reasoning, 2017, pp. 144–161. [Online]. Available: https://easychair.org/publications/paper/fPz
[56]
RTCA/DO-333, “Formal methods supplement to DO-178C and and DO-278A,” Washington, DC, Dec. 2011.
[57]
L. Wagner, “Automating DO-178C objectives with SpeAR: A case study,” in Proc. Safe Secure Syst. Softw. Symp., 2017. [Online]. Available: http://www.mys5.org/Proceedings/2017/Day_1/2017-S5-Day1_1335_Wagner.pdf
[58]
J. Rushby, “Software verification and system assurance,” in Proc. 7th Int. Conf. Softw. Eng. Formal Methods, Nov. 2009, pp. 3–10.
[59]
D. Hardin, D. R. Johnson, L. Wagner, and M. W. Whalen, “Development of security software: A high-assurance methodology,” in Proc. 11th Int. Conf. Formal Eng. Methods, Dec. 2009, pp. 266–285.
[60]
H. Chockler, O. Kupferman, R. P. Kurshan, and M. Y. Vardi, “A practical approach to coverage in model checking,” in Proc. Int. Conf. Comput. Aided Verification, 2001, pp. 66–78.
[61]
S. Das, A. Banerjee, P. Basu, P. Dasgupta, P. Chakrabarti, C. R. Mohan, and L. Fix, “Formal methods for analyzing the completeness of an assertion suite against a high-level fault model,” in Proc. 18th Int. Conf. VLSI Des. Held Jointly With 4th Int. Conf. Embedded Syst. Des., 2005, pp. 201–206.
[62]
K. Claessen, “A coverage analysis for safety property lists,” in Proc. Formal Methods Comput. Aided Des., 2007, pp. 139–145.
[63]
D. Große, U. Kühne, and R. Drechsler, “Estimating functional coverage in bounded model checking,” in Proc. Conf. Des. Autom. Test Eur., 2007, pp. 1176–1181.
[64]
H. Chockler, D. Kroening, and M. Purandare, “Coverage in interpolation-based model checking,” in Proc. 47th ACM/IEEE Des. Autom. Conf., 2010, pp. 182–187.
[65]
O. Kupferman, “Sanity checks in formal verification,” in Proc. 17th Int. Conf. Concurrency Theory, 2006, pp. 37–51.
[66]
L. Zhang, M. Gligoric, D. Marinov, and S. Khurshid, “Operator-based and random mutant selection: Better together,” in Proc. 28th IEEE/ACM Int. Conf. Automated Softw. Eng., Nov. 2013, pp. 92–102.
[67]
A. Cimatti, A. Griggio, and R. Sebastiani, “A simple and flexible way of computing small unsatisfiable cores in SAT modulo theories,” in Proc. Int. Conf. Theory Appl. Satisfiability Testing, 2007, pp. 334–339.
[68]
A. Nadel, V. Ryvchin, and O. Strichman, “Accelerated deletion-based extraction of minimal unsatisfiable cores,” J. Satisfiability Boolean Model. Comput., vol. 9, pp. 27–51, 2014.
[69]
A. Belov, H. Chen, A. Mishchenko, and J. Marques-Silva, “Core minimization in sat-based abstraction,” in Proc. Conf. Des. Autom. Test Eur., 2013, pp. 1411–1416.
[70]
A. Belov, I. Lynce, and J. Marques-Silva, “Towards efficient MUS extraction,” AI Commun., vol. 25, no. 2, pp. 97–116, 2012.
[71]
V. Ryvchin and O. Strichman, “Faster extraction of high-level minimal unsatisfiable cores,” in Theory and Applications of Satisfiability Testing. New York, NY, USA: Springer, 2011, pp. 174–187.
[72]
A. Belov, M. Janota, I. Lynce, and J. Marques-Silva, “On computing minimal equivalent subformulas,” in Principles and Practice of Constraint Programming. New York, NY, USA: Springer, 2012, pp. 158–174.
[73]
J. Marques-Silva, “Minimal unsatisfiability: Models, algorithms and applications,” in Proc. 40th IEEE Int. Symp. Multiple-Valued Logic, 2010, pp. 9–14.
[74]
A. Gupta, M. Ganai, Z. Yang, and P. Ashar, “Iterative abstraction using sat-based bmc with proof analysis,” in Proc. IEEE/ACM Int. Conf. Comput.-Aided Des., 2003, Art. no.
[75]
K. L. McMillan and N. Amla, “Automatic abstraction without counterexamples,” in Tools and Algorithms for the Construction and Analysis of Systems. New York, NY, USA: Springer, 2003, pp. 2–17.
[76]
H. Chen and J. Marques-Silva, “Improvements to satisfiability-based boolean function bi-decomposition,” in Proc. IEEE/IFIP 19th Int. Conf. VLSI Syst.-on-Chip, Oct. 2011, pp. 142–147.
[77]
M. H. Liffiton and K. A. Sakallah, “Algorithms for computing minimal unsatisfiable subsets of constraints,” J. Autom. Reasoning, vol. 40, no. 1, pp. 1–33, Jan. 2008. [Online]. Available: https://doi.org/10.1007/s10817-007-9084-z
[78]
J. Bailey and P. J. Stuckey, “Discovery of minimal unsatisfiable subsets of constraints using hitting set dualization,” in Proc. 7th Int. Conf. Practical Aspects Declarative Lang., 2005, pp. 174–186. [Online]. Available: https://doi.org/10.1007/978-3-540-30557-6_14
[79]
J. Bendík, “Consistency checking in requirements analysis,” in Proc. 26th ACM SIGSOFT Int. Symp. Softw. Testing Anal., 2017, pp. 408–411. [Online]. Available: http://doi.acm.org/10.1145/3092703.3098239
[80]
J. Bendík, N. Benes, J. Barnat, and I. Cerná, “Finding boundary elements in ordered sets with application to safety and requirements analysis,” in Proc. 14th Int. Conf. Softw. Eng. Formal Methods, 2016, pp. 121–136. [Online]. Available: https://doi.org/10.1007/978%E2%80%933-319-41591-8_9
[81]
J. Bendík, N. Benes, I. Cerná, and J. Barnat, “Tunable online MUS/MSS enumeration,” in Proc. 36th IARCS Annu. Conf. Found. Softw. Technol. Theoretical Comput. Sci., 2016, pp. 50:1–50:13. [Online]. Available: https://doi.org/10.4230/LIPIcs.FSTTCS.2016.50
[82]
A. Ivrii, A. Gurfinkel, and A. Belov, “Small inductive safe invariants,” in Proc. 14th Conf. Formal Methods Comput.-Aided Des., 2014, pp. 115–122.
[83]
Z. E. Hanna, P. A. M. Franzén, R. M. Weber, H. A. Farah, and R. K. Ranjan, “Formal verification coverage metrics for circuit design properties,” U.S. Patent 8826201, Sep. 2, 2014.
[84]
Synopsys VC Formal Platform. (2017). [Online]. Available: https://www.synopsys.com
[85]
M. Weiser, “Program slicing,” in Proc. 5th Int. Conf. Softw. Eng., 1981, pp. 439–449.
[86]
H. Agrawal and J. R. Horgan, “Dynamic program slicing,” ACM SIGPLAN Notices., vol. 25, no. 6, pp. 246–256, Jun. 1990.
[87]
H. F. Li, J. Rilling, and D. Goswami, “Granularity-driven dynamic predicate slicing algorithms for message passing systems,” Autom. Softw. Eng., vol. 11, no. 1, pp. 63–89, 2004.
[88]
A. Gurfinkel and M. Chechik, “Robust vacuity for branching temporal logic,” ACM Trans. Comput. Logic, vol. 13, no. 1, pp. 1:1–1:32, Jan. 2012.
[89]
H. Chockler and O. Strichman, “Before and after vacuity,” Formal Methods Syst. Des., vol. 34, no. 1, pp. 37–58, 2008. [Online]. Available: https://doi.org/10.1007/s10703-008-0060-y
[90]
S. Ben-David and O. Kupferman, “A framework for ranking vacuity results,” in Proc. 11th Int. Symp. Autom. Technol. Verification Anal., 2013, pp. 148–162.
[91]
H. Chockler and O. Strichman, “Easier and more informative vacuity checks,” in Proc. 5th IEEE/ACM Int. Conf. Formal Methods Models Codesign, 2007, pp. 189–198.
[92]
I. Beer, S. Ben-David, C. Eisner, and Y. Rodeh, in Proc. 9th Int. Conf. Comput. Aided Verification, 1997, pp. 279–290. [Online]. Available: https://doi.org/10.1007/3-540-63166-6_28
[93]
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. New York, NY, USA: Springer, 2015, pp. 279–294.
[94]
D. Schuler and A. Zeller, “Assessing oracle quality with checked coverage,” in Proc. 4th IEEE Int. Conf. Softw. Testing Verification Validation, 2011, pp. 90–99.
[95]
V. Schuppan and A. Biere, “Liveness checking as safety checking for infinite state spaces,” Electron. Notes Theoretical Comput. Sci., vol. 149, no. 1, pp. 79–96, Feb. 2006. [Online]. Available: https://doi.org/10.1016/j.entcs.2005.11.018
Index Terms
- Inductive Validity Cores
Index terms have been assigned to the content through auto-classification.
Recommendations
Efficient generation of inductive validity cores for safety properties
FSE 2016: Proceedings of the 2016 24th ACM SIGSOFT International Symposium on Foundations of Software EngineeringSymbolic 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 ...
Inductive Completeness of Logics of Programs
We propose a new approach to delineating logics of programs, based directly on inductive definition of program semantics. The ingredients are elementary and well-known, but their fusion yields a simple yet powerful approach, surprisingly overlooked for ...
Proving inductive validity of constrained inequalities
PPDP '16: Proceedings of the 18th International Symposium on Principles and Practice of Declarative ProgrammingRewriting induction (RI) frameworks consist of inference rules to prove equations to be inductive theorems of a given term rewriting system, i.e., to be inductively valid w.r.t. reduction of the given system. To prove inductive validity of inequalities ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
0098-5589 © 2019 IEEE. Personal use is permitted, but republication/redistribution requires IEEE permission. See https://www.ieee.org/publications/rights/index.html for more information.
Publisher
IEEE Press
Publication History
Published: 01 February 2021
Qualifiers
- Research-article
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 0Total Downloads
- Downloads (Last 12 months)0
- Downloads (Last 6 weeks)0
Reflects downloads up to 12 Dec 2024
Other Metrics
Citations
View Options
View options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in