Inheritance of Temporal Logic Properties

Abstract. Inheritance is one of the key features for the success of objectoriented 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 ...

• Type: Conference
• Year: 2003
• Where: FMOODS
• Authors: Heike Wehrheim
• Keywords: Correctness Properties, FMOODS 2003, FMOODS 2007, Re-use, Supports Incremental Design