Model Checking Abstract State Machines with Answer Set Programming

• Autorzy: Tang C.K.F. , Ternovska E.
• Języki publikacji: EN

Abstrakty

EN

The quality of a computer system can be enhanced by modelling its design and verifying the correctness of the design before implementation is done. Abstract State Machines (ASMs) provide a mathematical framework for system modelling, while Model Checking is a technology for verification of system properties. Together, they form a powerful tool for checking systems. Bounded Model Checking (BMC) based on Answer Set Programming (ASP) is a competitive model checking approach due to its ability to compactly encode BMC problems. In this paper, we present a method of applying ASP to BMC of ASMs. Given an ASM and a temporal property, we show how to efficiently translate the BMC problem for the ASM into a problem of answer set computation. Experimental results for our method using the answer set solvers SMODELS and CMODELS are also given.

Słowa kluczowe

EN

abstract state machines

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2007
• Tom: Vol. 77, nr 1,2
• Strony: 105--141
• Opis fizyczny: bibliogr. 27 poz., tab.

Twórcy

autor

Tang C.K.F.

autor

Ternovska E.

• School of Computing Science, Simon Fraser University, Burnaby, B.C., Canada,

Bibliografia

• [1] Y. Babovich, E. Erdem, and V. Lifschitz. Fages' theorem and answer set programming. In Proceedings of the 8th International Workshop on Non-Monotonic Reasoning, 2000.
• [2] Y. Babovich and V. Lifschitz. Computing answer sets using program completion. Unpublished draft, 2003.
• [3] C. Baral. Knowledge Representation, Reasoning, and Declarative Problem Solving. Cambridge University Press, 2003.
• [4] A. Biere, A. Cimatti, E. M. Clarke, O. Strichman, and Y. Zhu. Bounded Model Checking, volume 58 of Advances In Computers. Academic Press, 2003.
• [5] E. Börger and R. Stärk. Abstract State Machines: A Method for High-Level System Design and Analysis. Springer, 2003.
• [6] L. Carlucci Aiello and F. Massacci. Verifying security protocols as planning in logic programming. ACM Transactions on Computational Logic, 2(4):542-580, 2001.
• [7] W. Chan, R. Anderson, P. Beame, S. Burns, F. Modugno, D. Notkin, and J. Reese. Model checking large software specifications. IEEE Transactions on Software Engineering, 24(7):498-520, 1998.
• [8] A. Cimatti, E. Clarke, E. Giunchiglia, F. Giunchiglia, M. Pistore, M. Roveri, R. Sebastiani, and A. Tacchella. NuSMV 2: An opensource tool for symbolic model checking. In Proceedings of the 14th International Conference on Computer-Aided Verification, pages 359-364. Springer, 2002.
• [9] E. M. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press, 1999.
• [10] G. Del Castillo and K. Winter. Model checking support for the asm high-level language. In Proceedings of the 6th International Conference for Tools and Algorithms for the Construction and Analysis of Systems, pages 331-346. Springer, 2000.
• [11] Y. Dong, X. Du, Y. S. Ramakrishna, C. R. Ramakrishnan, I. V. Ramakrishnan, S. A. Smolka, O. Sokolsky, E. W. Stark, and D. S. Warren. Fighting livelock in the i-Protocol: A comparative study of verification tools. In Proceedings of the 5th International Conference on Tools and Algorithms, pages 74-88. Springer, 1999.
• [12] A. Gargantini, E. Riccobene, and S. Rinzivillo. Using Spin to generate tests from ASM specifications. In Proceedings of the 10th International Workshop on Abstract State Machines, pages 263-277. Springer, 2003.
• [13] A. Gawanmeh, S. Tahar, and K. Winter. Interfacing ASM with the MDG tool. In Proceedings of the 10th International Workshop on Abstract State Machines, pages 278-292. Springer, 2003.
• [14] M. Gelfond and V. Lifschitz. The stable model semantics for logic programming. In Proceedings of the 5th International Conference on Logic Programming, pages 1070-1080. MIT Press, 1988.
• [15] Y. Gurevich. Evolving algebras 1993: Lipari guide. In Egon Börger, editor, Specification and Validation Methods, pages 9-36. Oxford University Press, 1995.
• [16] K. Heljanko and I. Niemelä. Bounded LTL model checking with stable models. Theory and Practice of Logic Programming, 3(4):519-550, 2003.
• [17] T. Latvala, A. Biere, K. Heljanko, and T. Junttila. Simple is better: Efficient bounded model checking for past LTL. In Proceedings of the 6th International Conference on Verification, Model Checking and Abstract Interpretation, pages 380-395. Springer, 2005.
• [18] Yu. Lierler and M. Maratea. Cmodels-2: SAT-based answer set solver enhanced to non-tight programs. In Proceedings of the 7th Conference on Logic Programming and Non-Monotonic Reasoning, pages 346-350. Springer, 2004.
• [19] V. Lifschitz. Introduction to answer set programming, 2004. Introductory course at the 16th European Summer School in Logic, Language and Information.
• [20] K. L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993.
• [21] M. Moskewicz, C. Madigan, Y. Zhao, L. Zhang, and S. Malik. Chaff: Engineering an efficient SAT solver. In Proceedings of the 38th Design Automation Conference, pages 530-535. ACM Press, 2001.
• [22] P. Simons. Extending and Implementing the Stable Model Semantics. PhD thesis, Helsinki University of Technology, 2000.
• [23] T. Syrjänen. Lparse 1.0 User's Manual, 2000. Electronic manual available at http://www.tcs.hut.fi/Software/smodels/lparse.ps.
• [24] C. Tang. Model checking abstract state machines with answer set programming. Master's thesis, Simon Fraser University, 2006.
• [25] M. H. Van Emden and R. A. Kowalski. The semantics of predicate logic as a programming language. Journal of the ACM, 23(4):733-742, 1976.
• [26] J. Wing and M. Vaziri-Farahani. A case study in model checking software systems. Science of Computer Programming, 28(2-3):273-299, 1997.
• [27] K. Winter. Model Checking Abstract State Machines. PhD thesis, Technical University of Berlin, 2001.