Hybrid dynamic logic institutions for event/data-based systems

Hennicker, Rolf; Knapp, Alexander und Madeira, Alexandre (2021): Hybrid dynamic logic institutions for event/data-based systems. In: Formal Aspects of Computing, Bd. 33, Nr. 6: S. 1209-1248

Abstract

We propose E-down arrow((D) over right arrow)-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) over right arrow whose structures are used to model data states. E-down arrow((D) over right arrow)-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 e/psi where e is an event and psi a state transition predicate capturing the allowed reactions to the event. Towrite concrete specifications of recursive process structureswe 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 E-down arrow((D) over right arrow)-logic is powerful enough to characterise the semantics of an operational specification by a single E-down arrow((D) over right arrow)-sentence. Thus the whole (formal) development process for event/data-based systems relies on E-down arrow((D) over right arrow)-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.

• Dokumententyp: Zeitschriftenartikel
• Fakultät: Mathematik, Informatik und Statistik > Informatik
• Themengebiete: 000 Informatik, Informationswissenschaft, allgemeine Werke > 004 Informatik
• ISSN: 0934-5043
• Sprache: Englisch