Abstract
Answer Set Programming (ASP) has been demonstrated as an effective tool in various application areas, including formal verification. In this paper we present Bounded Model Checking (BMC) of Abstract State Machines (ASMs) based on ASP. We show how to succinctly translate an ASM and a temporal property into a logic program and solve the BMC problem for the ASM by computing an answer set for the corresponding program. Experimental results for our method using the answer set solvers SMODELS and CMODELS are also given.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Babovich, Y., Erdem, E., Lifschitz, V.: Fages’ theorem and answer set programming. In: Proceedings of the 8th International Workshop on Non-Monotonic Reasoning (2000)
Biere, A., Cimatti, A., Clarke, E.M., Strichman, O., Zhu, Y.: Bounded Model Checking. Advances In Computers, vol. 58. Elsevier, Amsterdam (2003)
Börger, E., Stärk, R.: Abstract State Machines: A Method for High-Level System Design and Analysis. Springer, New York (2003)
Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)
Del Castillo, G.: ASM-SL, a Specification Language based on Gurevich’s Abstract State Machines: Introduction and Language Definition. Heinz Nixdorf Institut Paderborn, Germany (1999)
Dong, Y., Du, X., Ramakrishna, Y.S., Ramakrishnan, C.R., Ramakrishnan, I.V., Smolka, S.A., Sokolsky, O., Stark, E.W., Warren, D.S.: Fighting livelock in the i-Protocol: A comparative study of verification tools. In: Proceedings of the 5th International Conference on Tools and Algorithms, pp. 74–88 (1999)
Van Emden, M.H., Kowalski, R.A.: The semantics of predicate logic as a programming language. Journal of the ACM 23(4), 733–742 (1976)
Gargantini, A., Riccobene, E., Rinzivillo, S.: Using Spin to generate tests from ASM specifications. In: Börger, E., Gargantini, A., Riccobene, E. (eds.) ASM 2003. LNCS, vol. 2589, pp. 263–277. Springer, Heidelberg (2003)
Heljanko, K., Niemelä, I.: Bounded LTL model checking with stable models. Theory and Practice of Logic Programming 3(4&5), 519–550 (2003)
Lierler, Y., Maratea, M.: 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, pp. 346–350 (2004)
Lifschitz, V.: Introduction to answer set programming. In: Introductory course at the 16th European Summer School in Logic, Language and Information (2004)
McMillan, K.L.: Symbolic Model Checking. Kluwer Academic Publishers, Norwell (1993)
Simons, P.: Extending and Implementing the Stable Model Semantics. PhD thesis, Helsinki University of Technology (2000)
Winter, K.: Model Checking Abstract State Machines. PhD thesis, Technical University of Berlin (2001)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Tang, C.K.F., Ternovska, E. (2005). Model Checking Abstract State Machines with Answer Set Programming. In: Sutcliffe, G., Voronkov, A. (eds) Logic for Programming, Artificial Intelligence, and Reasoning. LPAR 2005. Lecture Notes in Computer Science(), vol 3835. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11591191_31
Download citation
DOI: https://doi.org/10.1007/11591191_31
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-30553-8
Online ISBN: 978-3-540-31650-3
eBook Packages: Computer ScienceComputer Science (R0)