Modal specifications

Abstract

We present a theory of Modal Specifications which has been specifically designed in order to allow loose specifications to be expressed. Modal Specifications extends Process Algebra in the sense that specifications may be combined using process constructs. Moreover, Modal Specifications is given an operational interpretation imposing restrictions on the transitions of possible implementations by telling which transitions are necessary and which are admissable. This allows a refinement ordering between Modal Specifications to be defined extending the well-established notion of bisimulation. In the paper we present a logical characterization of the refinement-ordering and derive characteristic logical formulas from any given Modal Specifications. Also, we explore the possibility of combining Modal Specifications themselves logically, and we briefly comment on the automation of refinement.