=Paper=
{{Paper
|id=Vol-2951/keynote1
|storemode=property
|title=Specifying Event/Data-based Systems (keynote)
|pdfUrl=https://ceur-ws.org/Vol-2951/keynote1.pdf
|volume=Vol-2951
|authors=Alexander Knapp
|dblpUrl=https://dblp.org/rec/conf/csp/Knapp21
}}
==Specifying Event/Data-based Systems (keynote)==
<pdf width="1500px">https://ceur-ws.org/Vol-2951/keynote1.pdf</pdf>
<pre>
Specifying Event/Data-based Systems (keynote)
Alexander Knapp
Augsburg University, Germany


                                      Abstract
                                      Event/data-based systems are controlled by events, their local data state may change in reaction to events.
                                      Numerous methods and notations for specifying such reactive systems have been designed, though
                                      with varying focus on the different development steps and their refinement relations. We first briefly
                                      review some of such methods, like temporal/modal logic, TLA, UML state machines, symbolic transition
                                      systems, CSP, synchronous languages, and Event-B with their support for parallel composition and
                                      refinement. We then present E↓-logic for covering a broad range of abstraction levels of event/data-based
                                      systems from abstract requirements to constructive specifications in a uniform foundation. E↓-logic uses
                                      diamond and box modalities over structured events adopted from dynamic logic, for recursive process
                                      specifications it offers (control) state variables and binders from hybrid logic. The semantic interpretation
                                      relies on event/data transition systems; specification refinement is defined by model class inclusion.
                                      Constructive operational specifications given by state transition graphs can be characterised by a single
                                      E↓-sentence. Also a variety of implementation constructors is available in E↓-logic to support, among
                                      others, event refinement and parallel composition. Thus the whole development process can rely on
                                      E↓-logic and its semantics as a common basis.

                                      Acknowledgments: Joint work with Rolf Hennicker and Alexandre Madeira.




29th International Workshop on Concurrency, Specification and Programming (CS&P’21)
$ knapp@informatik.uni-augsburg.de (A. Knapp)
€ https://www.uni-augsburg.de/de/fakultaet/fai/informatik/prof/swtsse/ (A. Knapp)
 0000-0002-4050-3249 (A. Knapp)
                                    © 2021 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).
 CEUR
 Workshop
 Proceedings
               http://ceur-ws.org
               ISSN 1613-0073       CEUR Workshop Proceedings (CEUR-WS.org)

</pre>