Please use this identifier to cite or link to this item: http://hdl.handle.net/10773/26015
Title: A Hybrid Dynamic Logic for Event/Data-Based Systems
Author: Hennicker, Rolf
Madeira, Alexandre
Knapp, Alexander
Keywords: Dynamic Logic
Issue Date: 2019
Publisher: Springer
Abstract: We propose E↓ -logic as a formal foundation for the specification and development of event-based systems with local data states. The logic is intended to cover a broad range of abstraction levels from abstract requirements specifications up to constructive specifications. Our logic uses diamond and box modalities over structured actions adopted from dynamic logic. Atomic actions are pairs Open image in new window where e is an event and 𝜓/ψ a state transition predicate 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; specification refinement is defined by model class inclusion. 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↓-logic is powerful enough to characterise the semantics of an operational specification by a single E↓-sentence. Thus the whole development process can rely on E↓-logic and its semantics as a common basis. This includes also a variety of implementation constructors to support, among others, event refinement and parallel composition.
Peer review: yes
URI: http://hdl.handle.net/10773/26015
DOI: 10.1007/978-3-030-16722-6_5
ISBN: 978-3-030-16721-9
Appears in Collections:CIDMA - Capítulo de livro
AGG - Capítulo de livro

Files in This Item:
File Description SizeFormat 
1902.03074.pdf273.91 kBAdobe PDFView/Open


FacebookTwitterDeliciousLinkedInDiggGoogle BookmarksMySpace
Formato BibTex MendeleyEndnote Degois 

Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.