zbMATH — the first resource for mathematics

On the integration of observability and reachability concepts. (English) Zbl 1077.68709
Nielsen, Mogens (ed.) et al., Foundations of software science and computation structures. 5th international conference, FOSSACS 2002, held as part of the joint European conferences on theory and practice of software, ETAPS 2002, Grenoble, France, April 8–12, 2002. Proceedings. Berlin: Springer (ISBN 3-540-43366-X). Lect. Notes Comput. Sci. 2303, 21-36 (2002).
Summary: 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.
For the entire collection see [Zbl 0989.00051].

68Q65 Abstract data types; algebraic specification
68Q60 Specification and verification (program logics, model checking, etc.)
Full Text: Link