Debugging formal specifications: a practical approach using model-based diagnosis and counterstrategies

International Journal on Software Tools for Technology Transfer - Tập 15 - Trang 563-583 - 2011
Robert Könighofer1, Georg Hofferek1, Roderick Bloem1
1Institute for Applied Information Processing and Communications (IAIK), Graz University of Technology, Graz, Austria

Tóm tắt

Creating a formal specification for a design is an error-prone process. At the same time, debugging incorrect specifications is difficult and time consuming. In this work, we propose a debugging method for formal specifications that does not require an implementation. We handle conflicts between a formal specification and the informal design intent using a simulation-based refinement loop, where we reduce the problem of debugging overconstrained specifications to that of debugging unrealizability. We show how model-based diagnosis can be applied to locate an error in an unrealizable specification. The diagnosis algorithm computes properties and signals that can be modified in such a way that the specification becomes realizable, thus pointing out potential error locations. In order to fix the specification, the user must understand the problem. We use counterstrategies to explain conflicts in the specification. Since counterstrategies may be large, we propose several ways to simplify them. First, we compute the counterstrategy not for the original specification but only for an unrealizable core. Second, we use a heuristic to search for a countertrace, i.e., a single input trace which necessarily leads to a specification violation. Finally, we present the countertrace or the counterstrategy as an interactive game against the user, and as a graph summarizing possible plays of this game. We introduce a user-friendly implementation of our debugging method and present experimental results for GR(1) specifications.

Tài liệu tham khảo

Behrmann, G., Cougnard, A., David, A., Fleury, E., Larsen, K.G., Lime, D.: UPPAAL-Tiga: time for playing games! In: Proceedings of Computer Aided Verification (CAV’07), pp. 121–125 (2007)

Bloem, R., Cimatti, A., Greimel, K., Hofferek, G., Koenighofer, R., Roveri, M., Schuppan, V., Seeber, R.: RATSY—a new requirements analysis tool with synthesis. In: Proceedings of Computer Aided Verification. LNCS, vol. 6174, pp. 425–429 (2010)

Bloem, R., Galler, S., Jobstmann, B., Piterman, N., Pnueli, A., Weiglhofer, M.: Automatic hardware synthesis from specifications: a case study. In: Proceedings of the Design, Automation and Test in Europe, pp. 1188–1193 (2007)

Bloem, R., Galler, S., Jobstmann, B., Piterman, N., Pnueli, A., Weiglhofer, M.: Specify, compile, run: Hardware form PSL. In: 6th International Workshop on Compiler Optimization Meets Compiler Verification. Electronic Notes in Theoretical Computer Science (2007)

Bontemps Y., Schobbens P.-Y., Löding C.: Synthesis of open reactive systems from scenario-based specifications. Fundamamenta Informaticae 62(2), 139–169 (2004)

Bryant R.E.: Graph-based algorithms for Boolean function manipulation. IEEE Trans. Comput. C-35(8), 677–691 (1986)

Chatterjee, K., Henzinger, T., Jobstmann, B.: Environment assumptions for synthesis. In: International Conference on Concurrency Theory (CONCUR), pp. 147–161 (2008)

Chockler, H., Kupferman, O., Kurshan, R.P., Vardi, M. Y.: A practical approach to coverage in model checking. In: Berry, G., Comon, H., Finkel, A. (eds.) Thirteenth Conference on Computer Aided Verification (CAV’01). LNCS, vol. 2102, pp. 66–78. Springer, Berlin (2001)

Chockler, H., Kupferman, O., Vardi, M.Y.: Coverage metrics for temporal logic model checking. In: Tools and algorithms for the construction and analysis of systems (TACAS). LNCS, vol. 2031, pp. 528–542. Springer, Berlin (2001)

Cimatti, A., Clarke, E., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV Version 2: An OpenSource Tool for Symbolic Model Checking. In: Proceedings of the International Conference on Computer-Aided Verification (CAV’02) (2002)

Cimatti, A., Roveri, M., Schuppan, V., Tchaltsev, A.: Diagnostic information for realizability. In: Proceedings of Verification, Model Checking, and Abstract Interpretation (VMCAI’08), pp. 52–67 (2008)

Claessen, K.: A coverage analysis for safety property lists. In: Proceedings of Formal Methods in Computer Aided Design, pp. 139–145 (2007)

Console, L., Friedrich, G., Dupré, D. Theseider: Model-based diagnosis meets error diagnosis in logic programs. In: Proceedings of the International Joint Conference on Artificial Intelligence (IJCAI’93), pp. 1494–1499. Morgan-Kaufmann, Menlo Park (1993)

Das, S., Banerjee, A., Basu, P., Dasgupta, P., Chakrabarti, P.P., Mohan, C.R., Fix, L.: Formal methods for analyzing the completeness of an assertion suite against a high-level fault model. In: VLSI Design, pp. 201–206 (2005)

de Kleer J., Williams B.C.: Diagnosing multiple faults. Artif. Intell. 32, 97–130 (1987)

Dellacherie, S.: Automatic bus-protocol verification using assertions. In: Global Signal Processing Expo Conference (GSPx) (2004)

Felfernig A., Friedrich G., Jannach D., Stumptner M.: Consistency-based diagnosis of configuration knowledge bases. Artif. Intell. 152, 213–234 (2004)

Filiot, E., Jin, N., Raskin, J.-F.: An antichain algorithm for LTL realizability. In: Proceedings of Computer Aided Verification, pp. 263–277 (2009)

Fisman, D., Kupferman, O., Seinvald, S., Vardi, M.Y.: A framework for inverent vacuity. In: Proceedings of Haifa Verification Conference (HVC) (2008)

Friedrich, G., Shchekotykhin, K.M.: A general diagnosis method for ontologies. In: International Semantic Web Conference, pp. 232–246 (2005)

Friedrich G., Stumptner M., Wotawa F.: Model-based diagnosis of hardware designs. Artif. Intell. 111(1-2), 3–39 (1999)

Grädel, E., Thomas, W., Wilke, T. (eds): Automata, Logics, and Infinite Games: A Guide to Current Research. LNCS, vol. 2500. Springer (2002)

Große, D., Kühne, U., Drechsler, R.: Estimating functional coverage in bounded model checking. In: Proceedings of the Conference on Design Automation and Test in Europe (DATE’07), pp. 1176–1181 (2007)

Hoskote, Y., Kam, T., Ho, P.-H., Zhao, X.: Coverage estimation for symbolic model checking. In: Proceedings of Design Automation Conference, pp. 300–305 (1999)

Jobstmann, B., Bloem, R.: Optimizations for LTL synthesis. In: 6th Conference on Formal Methods in Computer Aided Design (FMCAD’06), pp. 117–124 (2006)

Katz, S., Grumberg, O., Geist, D.: “Have I written enough properties?”—A method of comparison between specification and implementation. In: Correct Hardware Design and Verification Methods (CHARME’99). LNCS, vol. 1703, pp. 280–297. Springer (1999)

Koenighofer, R., Hofferek, G., Bloem, R.: Debugging formal specifications using simple counterstrategies. In: Proceedings of Formal Methods in Computer Aided Design (FMCAD’09), pp. 152–159 (2009)

Koenighofer, R., Hofferek, G., Bloem, R.: Debugging unrealizable specifications with model-based diagnosis. In: Proceedings of Haifa Verification Conference (HVC). LNCS, vol. 6504, pp. 29–45. Springer, Berlin (2010)

Könighofer, R.: Debugging formal specifications with simplified counterstrategies. Master’s thesis, IAIK, Graz University of Technology, Inffeldgasse 16a, A-8010 Graz, Austria, (2009)

Kozen D.: Results on the propositional μ-calculus. Theor. Comput. Sci. 27, 333–354 (1983)

Kupferman, O., Vardi, M.Y.: Safraless decision procedures. In: Foundations of Computer Science, pp. 531–542 (2005)

Leucker, M.: Model checking games for the alternation-free μ-calculus and alternating automata. In: Proceedings of the International Conference on Logic Programming and Automated Reasoning (LPAR’99), pp. 77–91. Springer, Berlin (1999)

Leucker, M., Noll, T.: Truth/SLC—a parallel verification platform for concurrent systems. In: Computer Aided Verification, pp. 255–259. Springer, Berlin (2001)

Liffiton M.H., Sakallah K.A.: Algorithms for computing minimal unsatisfiable subsets of constraints. J. Autom. Reason. 40(1), 1–33 (2008)

Mateis, C., Stumptner, M., Wieland, D., Wotawa, F.: Model-based debugging of java programs. In: AADEBUG (2000)

Morgenstern, A., Schneider, K.: Exploiting the temporal logic hierarchy and the non-confluence property for efficient LTL synthesis. CoRR, abs/1006.1408 (2010)

Mori, R., Yonezaki, N.: Several realizability concepts in reactive objects. In: Information Modeling and Knowledge Bases (1993)

Pill, I., Semprini, S., Cavada, R., Roveri, M., Bloem, R., Cimatti, A.: Formal analysis of hardware requirements. In: Design Automation Conference, pp. 821–826 (2006)

Piterman, N., Pnueli, A., Sa’ar, Y.: Synthesis of reactive(1) designs. In: 7th International Conference on Verification, Model Checking and Abstract Interpretation. LNCS, vol. 3855, pp. 364–380. Springer, Berlin (2006)

Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: Proceedings Symposium on Principles of Programming Languages (POPL ’89), pp. 179–190 (1989)

Reiter R.: A theory of diagnosis from first principles. Artif. Intell. 32, 57–95 (1987)

Rosner, R.: Modular Synthesis of Reactive Systems. PhD thesis, Weizmann Institute of Science (1992)

Somenzi, F.: CUDD: CU Decision Diagram Package. University of Colorado at Boulder, ftp://vlsi.colorado.edu/pub/

Stevens, P., Stirling, C.: Practical model-checking using games. In: Tools and Algorithms for the Construction and Analysis of Systems. LNCS, vol. 1384. Springer, Berlin (1998)

Stirling, C.: Local model checking games. In: Proceedings of Concurrency Theory, pp. 1–11. Springer, Berlin (1995)

Stumptner, M., Wotawa, F.: Debugging functional programs. In: Proceedings on the 16th International Joint Conference on Artificial Intelligence (1999)

Tan, L.: PlayGame: A platform for diagnostic games. In: Computer Aided Verification. LNCS, vol. 3114, pp. 492–495. Springer, Berlin (2004)

Tripakis, S., Altisen, K.: On-the-fly controller synthesis for discrete and dense-time systems. In: World Congress on Formal Methods, pp. 233–252 (1999)

Yoshiura, N.: Finding the causes of unrealizability of reactive system formal specifications. In: Proceedings of Software Engineering and Formal Methods (SEFM’04), pp. 34–43 (2004)

Zeller A., Hildebrandt R.: Simplifying and isolating failure-inducing input. IEEE Trans. Softw. Eng. 28(2), 183–200 (2002)

Thông tin
Thông tin xuất bản

International Journal on Software Tools for Technology Transfer

Tập 15

563-583

Thông tin tác giả