Verifying for Reuse: Foundations of Object-Oriented System Verification.
José Luiz Fiadeiro, T. S. E. Maibaum · 1994
We propose an extended temporal logic framework, supporting modular verification over object-oriented specifications of reactive systems, with the aim of providing the possibility of reusing properties of components when the specifications of the components are themselves reused when building larger systems. For this purpose, we provide the means for component specifications to be inherited together with their properties (theorem reuse) and inference mechanisms (logic reuse). Our approach is based on an open semantics, the encapsulation mechanism of object-orientation, and the formalisation of the component-of relationship through theories and interpretations between theories (morphisms). 1 Introduction Reusability has become a key concern in software engineering. The basic idea is that one should be able to build complex systems out of predefined components, making the rest that will have to be engineered as small as possible. Verification is a key issue in reusability. The ...