Gastvortrag von Dr. Alexandre Madeira: Harnessing Hybrid and Dynamic Logics for Specification and Program Development

Uhrzeit: 10:15 - 11:45 Uhr
Ort: Raum F003 (Besprechungsraum PST), Oet. 67

Alexandre Madeira
HASLab, INESC TEC
University of Minho, Portugal
(joint work with R. Hennicker, M.A. Maritns and L.S. Barbosa)

In the first part of this talk we give a brief overview on our previous work on the use of hybrid logics as a specification formalism for reactive and reconfigurable systems. We depict a systematic method to build hybrid logics "on-demand", by developing the hybrid features (nominals, satisfaction operators and multi-modalities) as well as the corresponding modal semantics, on top of any base logic that forms an institution, like equational logic, first-order-logic, Fuzzy logic, etc. Suitable bisimulation notions and refinement notions for generic hybridised logics are considered.    

Then we discuss the exercise of finding a uniform logic that supports the development of reactive systems on various levels of abstraction, from property specifications, concerning e.g. safety and liveness requirements, to constructive specifications representing concrete programs.  This is achieved by combining features of both hybrid and dynamic logics in the same formalism: regular expressions of actions - inherent to dynamic logic - allow the specification of abstract requirements; nominals - a feature of hybrid logic - allow to specify concrete relational structures. A systematic translation from a process algebra into a constructive fragment of this logic is provided. The verification of abstract properties in the concrete models provides a proof method for refinement correctness w.r.t. model class inclusion.