On the integration of observability and reachability concepts

Abstract

This paper focuses on the integration of reachability and observability concepts within an algebraic, institution-based framework. We develop the essential notions that are needed to construct an institution which takes into account both the generation- and observation-oriented aspects of software systems. Thereby the underlying paradigm is that the semantics of a specification should be as loose as possible to capture all its correct realizations. We also consider the so-called “idealized models” of a specification which are useful to study the behavioral properties a user can observe when he/she is experimenting with the system. Finally, we present sound and complete proof systems that allow us to derive behavioral properties from the axioms of a given specification.