ETAPS 2019
Sat 6 - Thu 11 April 2019 Prague, Czech Republic
Tue 9 Apr 2019 12:00 - 12:30 at JUPITER - Software Verification I Chair(s): Wil van der Aalst

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 regular expressions of actions adopted from dynamic logic. Atomic actions are pairs e / ψ where e is an event and ψ a state transition predicate. To write concrete specifications of recursive process structures we integrate 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.

Tue 9 Apr

fase-2019-papers
10:30 - 12:30: FASE 2019 - Software Verification I at JUPITER
Chair(s): Wil van der AalstRWTH Aachen
fase-2019-papers10:30 - 11:00
Talk
Tobias RungeTU Braunschweig, Ina SchaeferTechnische Universität Braunschweig, Loek CleophasEindhoven University of Technology (TU/e) and Stellenbosch University (SU), Thomas ThümTU Braunschweig, Germany, Derrick KourieStellenbosch University, Bruce W Watson
Link to publication
fase-2019-papers11:00 - 11:30
Talk
Joonyoung Park, Alexander JordanOracle Labs, Australia, Sukyoung RyuKAIST, South Korea
Link to publication
fase-2019-papers11:30 - 12:00
Talk
Min ZhangEast China Normal University, Fu Song, Frederic MalletUniversité Côte d'Azur, France, Xiaohong Chen
Link to publication
fase-2019-papers12:00 - 12:30
Talk
Rolf HennickerLudwig Maximilians University Munich, Germany, Alexandre Madeira, Alexander Knapp
Link to publication