Hybrid dynamic logic institutions for event/data-based systems

Abstract

We propose ED-logic as a formal foundation for the specification and development of event-based systems with data states. The framework is presented as an institution in the sense of Goguen and Burstall and the logic itself is parametrised by an underlying institution D whose structures are used to model data states. ED-logic is intended to cover a broad range of abstraction levels from abstract requirements specifications up to constructive specifications. It uses modal diamond and box operators over complex actions adopted from dynamic logic. Atomic actions are pairs of events and state transition predicates capturing the allowed reactions to the event. To write concrete specifications of recursive process structures we integrate (control) state variables and binders of hybrid logic. The semantic interpretation relies on event/data transition systems. For the presentation of constructive specifications we propose operational event/data specifications allowing for familiar, diagrammatic representations by state transition graphs. We show that ED-logic is powerful enough to characterise the semantics of an operational specification by a single ED-sentence. Thus the whole (formal) development process for event/data-based systems relies on ED-logic and its semantics as a common basis. It is supported by a variety of implementation constructors which can express, among others, event refinement and parallel composition. Due to the genericity of the approach, it is also possible to change a data state institution during system development when needed. All steps of our formal treatment are illustrated by a running example.