Abstract
An interactive theorem proving method for the verification of infinite state transition systems is described.
The state space of a transition system is defined as a quotient set (i.e. a set of equivalence classes) of terms of a topmost sort State, and the transitions are defined with conditional rewrite rules over the quotient set. A property to be verified is either (1) an invariant (i.e. a state predicate that is valid for all reachable states) or (2) a (p leads-to q) property for two state predicates p and q, where (p leads-to q) means that from any reachable state s with (p(s) = true) the system will get into a state t with (q(t) = true) no matter what transition sequence is taken.
Verification is achieved by developing proof scores in CafeOBJ . Sufficient verification conditions are formalized for verifying invariants and (p leads-to q) properties. For each verification condition, a proof score is constructed to (1) generate a finite set of state patterns that covers all possible infinite states and (2) check validity of the verification condition for all the covering state patterns by reductions.
The method achieves significant automation of proof score developments.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Bae, K., Escobar, S., Meseguer, J.: Abstract logical model checking of infinite-state systems using narrowing. In: van Raamsdonk, F. (ed.) RTA. LIPIcs, vol. 21, pp. 81–96. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2013)
Baier, C., Katoen, J.P.: Principles of model checking, pp. 1–975. MIT Press (2008)
CafeOBJ (2014), http://cafeobj.org/ , http://www.ldl.jaist.ac.jp/cafeobj/
Chandy, K.M., Misra, J.: Parallel program design - a foundation. Addison-Wesley (1989)
Clarke, E.M., Grumberg, O., Peled, D.: Model checking. MIT Press (2001)
Coq (2014), http://coq.inria.fr
Dong, J.S., Zhu, H. (eds.): ICFEM 2010. LNCS, vol. 6447. Springer, Heidelberg (2010)
Escobar, S., Meseguer, J.: Symbolic model checking of infinite-state systems using narrowing. In: Baader, F. (ed.) RTA 2007. LNCS, vol. 4533, pp. 153–168. Springer, Heidelberg (2007)
Futatsugi, K.: Verifying specifications with proof scores in CafeOBJ. In: Proc. of 21st IEEE/ACM International Conference on Automated Software Engineering (ASE 2006), pp. 3–10. IEEE Computer Society (2006)
Futatsugi, K.: Fostering proof scores in CafeOBJ. In: Dong, Zhu (eds.) [7], pp. 1–20
Futatsugi, K., Găină, D., Ogata, K.: Principles of proof scores in CafeOBJ. Theor. Comput. Sci. 464, 90–112 (2012)
Goguen, J.A., Meseguer, J.: Order-sorted algebra I: Equational deduction for multiple inheritance, overloading, exceptions and partial operations. Theor. Comput. Sci. 105(2), 217–273 (1992)
Grumberg, O., Veith, H. (eds.): 25 Years of Model Checking. LNCS, vol. 5000. Springer, Heidelberg (2008)
Guttag, J.V., Horning, J.J., Garland, S.J., Jones, K.D., Modet, A., Wing, J.M.: Larch: Languages and Tools for Formal Specification. Springer (1993)
HOL (2014), http://hol.sourceforge.net
Maude (2014), http://maude.cs.uiuc.edu/
Meseguer, J.: Twenty years of rewriting logic. J. Log. Algebr. Program. 81(7-8), 721–781 (2012)
Nakamura, M., Ogata, K., Futatsugi, K.: Incremental proofs of termination, confluence and sufficient completeness of OBJ specifications. In: Iida, S., Meseguer, J., Ogata, K. (eds.) Specification, Algebra, and Software. LNCS, vol. 8373, pp. 92–109. Springer, Heidelberg (2014)
Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL. LNCS, vol. 2283. Springer, Heidelberg (2002)
Ogata, K., Futatsugi, K.: Proof scores in the oTS/CafeOBJ method. In: Najm, E., Nestmann, U., Stevens, P. (eds.) FMOODS 2003. LNCS, vol. 2884, pp. 170–184. Springer, Heidelberg (2003)
Ogata, K., Futatsugi, K.: Simulation-based verification for invariant properties in the OTS/CafeOBJ method. Electr. Notes Theor. Comput. Sci. 201, 127–154 (2008)
Ogata, K., Futatsugi, K.: A combination of forward and backward reachability analysis methods. In: Dong, Zhu (eds.) [7], pp. 501–517 (2010)
PVS (2014), http://pvs.csl.sri.com
Rocha, C., Meseguer, J.: Proving safety properties of rewrite theories. technical report. Tech. rep., University of Illinois at Urbana-Champaign (2010)
Rocha, C., Meseguer, J.: Proving safety properties of rewrite theories. In: Corradini, A., Klin, B., Cîrstea, C. (eds.) CALCO 2011. LNCS, vol. 6859, pp. 314–328. Springer, Heidelberg (2011)
TeReSe (ed.): Term Rewriting Systems. Cambridge Tracts in Theoretical Computer Science, vol. 55. Cambridge University Press (2003)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this chapter
Cite this chapter
Futatsugi, K. (2015). Generate & Check Method for Verifying Transition Systems in CafeOBJ . In: De Nicola, R., Hennicker, R. (eds) Software, Services, and Systems. Lecture Notes in Computer Science, vol 8950. Springer, Cham. https://doi.org/10.1007/978-3-319-15545-6_13
Download citation
DOI: https://doi.org/10.1007/978-3-319-15545-6_13
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-15544-9
Online ISBN: 978-3-319-15545-6
eBook Packages: Computer ScienceComputer Science (R0)