Inheritance of Temporal Logic Properties
Inheritance is one of the key features for the success of object-oriented languages. Inheritance (or specialisation) supports incremental design and re-use of already written specifications or programs. In a formal approach to system design the interest does not only lie in re-use of class definitions but also in re-use of correctness proofs. If a provably correct class is specialised we like to know those correctness properties which are preserved in the subclass. This can avoid re-verification of already proven properties and may thus substantially reduce the verification effort.
In this paper we study the question of inheritance of correctness properties in the context of state-based formalisms, using a temporal logic (CTL) to formalise requirements on classes. Given a superclass and its specialised subclass we develop a technique for computing the set of formulas which are preserved in the subclass. For specialisation we allow addition of attributes, modification of existing as well as extension with new methods.
KeywordsTemporal Logic Atomic Proposition Correctness Proof Kripke Structure Correctness Property
- 2.Clarke, E., Grumberg, O., Peled, D.: Model checking. MIT Press, Cambridge (1999)Google Scholar
- 7.Hatcliff, J., Dwyer, M., Zheng, H.: Slicing software for model construction. Higher-order and Symbolic Computation (to appear)Google Scholar
- 8.Huizing, K., Kuiper, R.: Reinforcing fragile base classes. In: Poetzsch-Heffter, A. (ed.) Workshop on Formal Techniques for Java Programs, ECOOP 2001 (2001)Google Scholar
- 11.Oda, T., Araki, K.: Specification slicing in formal methods of software development. In: Proceedings of the Seventeenth Annual International Computer Software & Applications Conference, pp. 313–319. IEEE Computer Society Press, Los Alamitos (1993)Google Scholar
- 12.Poetzsch-Heffter, A., Meyer, J.: Interactive verification environments for objectoriented languages. Journal of Universal Computer Science 5(3), 208–225 (1999)Google Scholar
- 14.van Glabbeek, R., Weijland, W.P.: Refinement in branching time semantics. In: Proc. IFIP Conference, pp. 613–618. North-Holland Publishing Company, Amsterdam (1989)Google Scholar
- 15.Wehrheim, H.: Behavioural subtyping and property preservation. In: Smith, S., Talcott, C. (eds.) FMOODS 2000: Formal Methods for Open Object-Based Distributed Systems. Kluwer, Dordrecht (2000)Google Scholar