Abstract
We use hidden algebra as a formal framework for object paradigm. We introduce a labeled transition system for each object specification model, and then define a suitable notion of bisimulation over these models. The labeled transition systems are used to define CTL models of object specifications. Given two hidden algebra models of an object specification, the bisimilar states satisfy the same set of CTL formulas. We build a canonical CTL model directly from the object specification. Using this CTL model, we can verify the temporal properties using a software tool allowing SMV model checking.
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
Bidoit, M., Hennicker, R., Kurz, A.: Observational logic, constructor-based logic, and their duality. Theoretical Computer Science 298(3), 471–510 (2003)
BOBJ home page, http://www.cs.ucsd.edu/groups/tatami/bobj/
Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (2000)
Goguen, J., Malcolm, G.: A hidden agenda. Theoretical Computer Science 245(1), 55–101 (2000)
Goguen, J., Lin, K., Rosu, G.: Circular Coinductive Rewriting. In: Proceedings, Automated Software Engineering 2000, pp. 123–131. IEEE Press, Los Alamitos (2000)
Hennicker, R., Bidoit, M.: Observational logic. In: Haeberer, A.M. (ed.) AMAST 1998. LNCS, vol. 1548, pp. 263–277. Springer, Heidelberg (1998)
Lucanu, D., Ciobanu, G.: Behavioral Bisimulation and CTL Models for Hidden Algebraic Specifications. “A.I.Cuza” University of Iaşi, Faculty of Computer Science, TR 03–03 (2003), www.infoiasi.ro/~tr/tr.pl.cgi
Rösiger, M.: Coalgebras and Modal Logic. Electronic Notes in Theoretical Computer Science, vol. 33 (2000)
Roşu, G.: Hidden Logic. PhD thesis, University of California at San Diego (2000)
Wirsing, M.: Algebraic Specification. In: Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics, pp. 675–788. Elsevier, Amsterdam (1990)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Lucanu, D., Ciobanu, G. (2004). Model Checking for Object Specifications in Hidden Algebra. In: Steffen, B., Levi, G. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2004. Lecture Notes in Computer Science, vol 2937. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-24622-0_10
Download citation
DOI: https://doi.org/10.1007/978-3-540-24622-0_10
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-20803-7
Online ISBN: 978-3-540-24622-0
eBook Packages: Springer Book Archive