1990 | ReviewPaper | Buchkapitel
Modal specifications
verfasst von : Kim Guldstrand Larsen
Erschienen in: Automatic Verification Methods for Finite State Systems
Verlag: Springer Berlin Heidelberg
Enthalten in: Professional Book Archive
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
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.