Preserving Properties Under Change

In this paper we discuss the question which properties of a formally verified component are preserved when the component is changed due to an adaption to a new use. More specifically, we will investigate when a temporal logic property of an Object-Z class is preserved under a modification or extension of the class with new features. To this end, we use the slicing technique from program analysis which provides us with a representation of the dependencies within the class in the form of a program dependence graph. This graph can be used to determine the effect of a change to the class’ behaviour and thus to the holding of a temporal logic formula.

• Type: Conference
• Year: 2003
• Where: FMCO
• Authors: Heike Wehrheim
• Keywords: FMCO 2003, Object-Z Class, Temporal Logic, Temporal Logic Property