The Community for Technology Leaders
RSS Icon
Subscribe
Issue No.06 - June (2013 vol.62)
pp: 1234-1254
T. Nopper , Dept. of Comput. Sci., Univ. of Freiburg, Freiburg, Germany
C. Scholl , Dept. of Comput. Sci., Univ. of Freiburg, Freiburg, Germany
ABSTRACT
We consider the problem of checking whether an incomplete design (i.e., a design containing "unknown parts", so-called Black Boxes) can still be extended to a complete design satisfying a given property or whether the property is satisfied for all possible extensions. There are many applications of property checking for incomplete designs, such as early verification checks for unfinished designs, error localization in faulty designs and the abstraction of complex parts of a design in order to simplify the property checking task. To process incomplete designs we present an approximate, yet sound algorithm. The algorithm is flexible in the sense that for every Black Box a different approximation method can be chosen. This permits us to handle less relevant Black Boxes (in terms of the property) with larger approximation and thus faster, whereas we do not lose important information when the possible effect of more relevant Black Boxes is modeled by more exact methods. Additionally, we present a concept to decide exactly whether Black Boxes with bounded memory can be implemented so that they satisfy a given property. This question is reduced to conventional symbolic model checking. The effectiveness and feasibility of the methods is demonstrated by a series of experimental results.
INDEX TERMS
formal verification, approximation theory, binary decision diagrams, symbolic model checking, incomplete design, black box, property checking, verification checks, unfinished designs, error localization, faulty design, approximation method, exact method, bounded memory, Computational modeling, Boolean functions, Approximation methods, Logic gates, Data structures, Integrated circuit modeling, Algorithm design and analysis, BDDs, Symbolic model checking, verification, Black Boxes, incomplete designs, abstraction, approximation
CITATION
T. Nopper, C. Scholl, "Symbolic Model Checking for Incomplete Designs with Flexible Modeling of Unknowns", IEEE Transactions on Computers, vol.62, no. 6, pp. 1234-1254, June 2013, doi:10.1109/TC.2012.53
REFERENCES
[1] C. Scholl and B. Becker, "Checking Equivalence for Partial Implementations," Proc. Design Automation Conf., pp. 238-243, 2001.
[2] T. Nopper and C. Scholl, "Approximate Symbolic Model Checking for Incomplete Designs," Proc. Formal Methods in Computer-Aided Design Conf. (FMCAD), pp. 290-305, Nov. 2004.
[3] E.M. Clarke, E.A. Emerson, and A.P. Sistla, "Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications," ACM Trans. Programming Languages and Systems, vol. 8, no. 2, pp. 244-263, 1986.
[4] R.E. Bryant, "Graph—Based Algorithms for Boolean Function Manipulation," IEEE Trans. Computers, vol. C-35, no. 8, pp. 677-691, Aug. 1986.
[5] J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, and L.J. Hwang, "Symbolic Model Checking: $10^{20}$ States and Beyond," Information and Computation, vol. 98, no. 2, pp. 142-170, 1992.
[6] K.L. McMillan, Symbolic Model Checking. Kluwer Academic Publisher, 1993.
[7] A. Pnueli and R. Rosner, "On the Synthesis of a Reactive Module," Proc. ACM Symp. Principles of Programming Languages, pp. 179-190, 1989.
[8] E. Asarin, O. Maler, and A. Pnueli, "Symbolic Controller Synthesis for Discrete and Timed Systems," Proc. Hybrid Systems Conf., pp. 1-20, 1995.
[9] A. Pnueli and R. Rosner, "Distributed Systems are hard to Synthesize," Proc. IEEE Symp. Foundations of Computer Science, pp. 746-757, 1990.
[10] The VIS Group, "VIS: A System for Verification and Synthesis," Proc. Eighth Int'l Conf. Computer Aided Verification (CAV), pp. 428-432, 1996.
[11] K.G. Larsen and B. Thomsen, "A Modal Process Logic," Proc. Third Ann. Symp. Logic in Computer Science (LICS), pp. 203-210, 1988.
[12] G. Bruns and P. Godefroid, "Model Checking Partial State Spaces with 3-Valued Temporal Logics," Proc. 11th Int'l Conf. Computer Aided Verification (CAV), pp. 274-287, 1999.
[13] M. Huth, R. Jagadeesan, and D. Schmidt, "Modal Transition Systems: A Foundation for Three-Valued Program Analysis," Proc. European Symp. Programming, pp. 155-169, Apr. 2001.
[14] C.-J. H. Seger and R.E. Bryant, "Formal Verification by Symbolic Evaluation of Partially-Ordered Trajectories," Formal Methods in System Design, vol. 6, no. 2, pp. 147-189, Mar. 1995.
[15] J.R. Burch and D.L. Dill, "Automatic Verification of Microprocessor Control," Proc. Int'l Conf. Computer Aided Verification (CAV), pp. 68-80, 1994.
[16] R. Kurshan, Computer-Aided Verification of Coordinating Processes. Princeton Univ. Press, 1994.
[17] B. Li, C. Wang, and F. Somenzi, "Abstraction Refinement in Symbolic Model Checking Using Satisfiability as the only Decision Procedure," Int'l J. Software Tools for Technology Transfer, vol. 7, no. 2, pp. 143-155, 2005.
[18] D. Kroening, "Computing Over-Approximations with Bounded Model Checking," Electronic Notes in Theoretical Computer Science, vol. 144, no. 1, pp. 79-92, 2006.
[19] R.E. Bryant, "Symbolic Boolean Manipulation with Ordered Binary Decision Diagrams," ACM Computing Surveys, vol. 24, pp. 293-318, 1992.
[20] M. Abramovici, M.A. Breuer, and A.D. Friedman, Digital Systems Testing and Testable Design. CS Press, 1990.
[21] A. Jain, V. Boppana, R. Mukherjee, J. Jain, M. Fujita, and M. Hsiao, "Testing, Verification, and Diagnosis in the Presence of Unknowns," Proc. IEEE 18th VLSI Test Symp., pp. 263-269, 2000.
[22] T. Filkorn, "Functional Extension of Symbolic Model Checking," Proc. Int'l Conf. Computer Aided Verification (CAV), pp. 225-232, 1992.
[23] P.F. Williams, A. Biere, E.M. Clarke, and A. Gupta, "Combining Decision Diagrams and SAT Procedures for Efficient Symbolic Model Checking," Proc. Int'l Conf. Computer Aided Verification (CAV), pp. 124-138, 2000.
[24] F. Somenzi, CUDD: CU Decision Diagram Package Release 2.3.1, Univ. of Colorado, 2001.
[25] H. Higuchi and F. Somenzi, "Lazy Group Sifting for Efficient Symbolic State Traversal of FSMs," Proc. Int'l Conf. Computer Aided Verification (CAV), pp. 45-49, 1999.
[26] R. Hojati, S.C. Krishnan, and R.K. Brayton, "Early Quantification and Partitioned Transition Relations," Proc. IEEE Int'l Conf. Computer Design, pp. 12-19, 1996.
[27] E. Clarke, O. Grumberg, and D. Peled, Model Checking. MIT Press, 1999.
[28] E. Sentovich, K. Singh, L. Lavagno, C. Moon, R. Murgai, A. Saldanha, H. Savoj, P. Stephan, R.K. Brayton, and A.L. Sangiovanni-Vincentelli, "SIS: A System for Sequential Circuit Synthesis," technical report, Univ. of Berkeley, 1992.
[29] A. Cimatti, E.M. Clarke, F. Giunchiglia, and M. Roveri, "Nusmv: A New Symbolic Model Verifier," Proc. Int'l Conf. Computer Aided Verification (CAV), pp. 495-499, 1999.
[30] K.L. McMillan, The SMV Language, Cadence Berkeley Labs, 1999.
[31] K.L. McMillan, The SMV System—For SMV Version 2.5.4, Carnegie Mellon Univ., 2000.
[32] T. Villa, G. Swamy, and T. Shiple, VIS User's Manual, Electronics Research Laboratory, Univ. of Colorado at Boulder, 1996.
[33] R. Milner, "An Algebraic Definition of Simulation Between Programs," Proc. Second Int'l Joint Conf. Artificial Intelligence, pp. 481-489, 1971.
[34] D. Park, "Concurrency and Automata on Infinite Sequences," Proc. Fifth GI-Conf. Theoretical Computer Science, pp. 167-183, 1981.
[35] C.-J. H. Seger, R.B. Jones, J.W. O'Leary, T.F. Melham, M. Aagaard, C. Barrett, and D. Syme, "An Industrially Effective Environment for Formal Hardware Verification." IEEE Trans. Computers, vol. 24, no. 9, pp. 1381-1405, Sept. 2005.
[36] S. Berezin, A. Biere, E.M. Clarke, and Y. Zhu, "Combining Symbolic Model Checking with Uninterpreted Functions for Out-Of-Order Processor Verification," Proc. Second Int'l Conf. Formal Methods in Computer-Aided Design (FMCAD), pp. 369-386, 1998.
[37] R.E. Bryant, S. German, and M.N. Velev, "Processor Verification Using Efficient Reductions of the Logic of Uninterpreted Functions to Propositional Logic," ACM Trans. Computational Logic, vol. 2, no. 1, pp. 1-41, 2001.
[38] S.K. Lahiri, S.A. Seshia, and R.E. Bryant, "Modeling and Verification of Out-of-Order Microprocessors in UCLID," Proc. Fourth Int'l Conf. Formal Methods in Computer-Aided Design (FMCAD), pp. 142-159, 2002.
[39] A. Biere, A. Cimatti, E.M. Clarke, and Y. Zhu, "Symbolic Model Checking without BDDs," Proc. Fifth Int'l Conf. Tools and Algorithms for the Construction and Analysis of Systems, 1999.
[40] M. Sheeran, S. Singh, and G. Stålmarck, "Checking Safety Properties Using Induction and a SAT-Solver," Proc. Int'l Conf. Formal Methods in Computer-Aided Design, pp. 407-420, 2000.
[41] K.L. McMillan, "Interpolation and SAT-Based Model Checking," Proc. Int'l Conf. Computer Aided Verification (CAV), 2003.
[42] D. Wang, P.-H. Ho, J. Long, J. Kukula, Y. Zhu, T. Ma, and R. Damiano, "Formal Property Verification by Abstraction Refinement with Formal, Simulation and Hybrid Engines," Proc. Design Automation Conf. (DAC), pp. 35-40, 2001.
[43] C. Wang, B. Li, H. Jin, G.D. Hachtel, and F. Somenzi, "Improving Ariadne's Bundle by Following Multiple Threads in Abstraction Refinement," Proc. IEEE/ACM Int'l Conf. Computer-Aided Design (ICCAD), pp. 408-415, 2003.
[44] E.M. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith, "Counterexample-Guided Abstraction Refinement," Proc. Int'l Conf. Computer Aided Verification (CAV), pp. 154-169, 2000.
[45] K.G. Larsen and L. Xinxin, "Equation Solving Using Modal Transition Systems," Proc. IEEE Fifth Ann. Symp. Logic in Computer Science (LICS), pp. 108-117, 1990.
[46] G. Bruns and P. Godefroid, "Generalized Model Checking: Reasoning about Partial State Spaces," Proc. Int'l Conf. Concurrency Theory, pp. 168-182, 2000.
[47] P. Godefroid and R. Jagadeesan, "On the Expressiveness of 3-Valued Models," Proc. Fourth Int'l Conf. Verification, Model Checking, and Abstract Interpretation (VMCAI), pp. 206-222, 2003.
[48] A. Gurfinkel and M. Chechik, "How Thorough is Thorough Enough?" Proc. 13 IFIP WG 10.5 Int'l Conf. Correct Hardware Design and Verification Methods (CHARME), pp. 65-80, 2005.
[49] A. Gurfinkel, O. Wei, and M. Chechik, "Systematic Construction of Abstractions for Model-Checking," Proc. Seventh Int'l Conf. Verification, Model Checking, and Abstract Interpretation (VMCAI), pp. 381-397, 2006.
[50] S. Shoham and O. Grumberg, "Monotonic Abstraction-Refinement for Ctl," Proc. Tools and Algorithms for Construction and Analysis of Systems Conf. (TACAS), pp. 546-560, 2004.
[51] O. Wei, A. Gurfinkel, and M. Chechik, "Mixed Transition Systems Revisited," Proc. 10th Int'l Conf. Verification, Model Checking, and Abstract Interpretation (VMCAI), pp. 349-365, 2009.
[52] D. Dams, R. Gerth, and O. Grumberg, "Abstract Interpretation of Reactive Systems," ACM Trans. Programming Languages and Systems, vol. 19, no. 2, pp. 253-291, 1997.
[53] P. Godefroid, M. Huth, and R. Jagadeesan, "Abstraction-Based Model Checking Using Modal Transition Systems," Proc. 12th Int'l Conf. Concurrency Theory (CONCUR), pp. 426-440, 2001.
[54] M. Chechik, B. Devereux, S.M. Easterbrook, and A. Gurfinkel, "Multi-Valued Symbolic Model-Checking," ACM Trans. Software Eng. and Methodology, vol. 12, no. 4, pp. 371-408, 2003.
[55] W. Chan, "Temporal-Logic Queries," Proc. Int'l Conf. Computer Aided Verification (CAV), pp. 450-463, 2000.
[56] A. Gurfinkel, M. Chechik, and B. Devereux, "Temporal Logic Query Checking: A Tool for Model Exploration," IEEE Trans. Software Eng., vol. 29, no. 10, pp. 898-914, Oct. 2003.
[57] I. Beer, S. Ben-David, C. Eisner, and Y. Rodeh, "Efficient Detection of Vacuity in Temporal Model Checking," Formal Methods System Design, vol. 18, no. 2, pp. 141-163, 2001.
[58] A. Gurfinkel and M. Chechik, "How Vacuous is Vacuous?" Proc. Tools and Algorithms for Construction and Analysis of Systems Conf. (TACAS), pp. 451-466, 2004.
[59] A. Gurfinkel and M. Chechik, "Multi-Valued Model Checking via Classical Model Checking," Proc. Int'l Conf. Concurrency Theory (CONCUR), pp. 263-277, 2003.
[60] B. Jobstmann, A. Griesmayer, and R. Bloem, "Program Repair as a Game," Proc. Int'l Conf. Computer Aided Verification (CAV), pp. 226-238, 2005.
[61] N. Yevtushenko, T. Villa, R.K. Brayton, A. Petrenko, and A.L. Sangiovanni-Vincentelli, "Solution of Parallel Language Equations for Logic Synthesis," Proc. IEEE Int'l Conf. Computer-Aided Design, pp. 103-110, 2001.
83 ms
(Ver 2.0)

Marketing Automation Platform Marketing Automation Tool