• TUCS Publication Series
• How to Publish in TUCS Series
• Publication Search
• Publication Graph
• Publication Input
• Publication Input Guide
• JuFo Browser

Integrating Refinement-Based Methods for Developing Timed Systems

Jüri Vain, Leonidas Tsiopoulos, Pontus Boström, Integrating Refinement-Based Methods for Developing Timed Systems. In: Luigia Petre, Emil Sekerinski (Eds.), From Action Systems to Distributed Systems: The Refinement Approach, 171 – 185, Taylor & Francis, 2016.

http://dx.doi.org/10.1201/b20053-17

Abstract:

Refinement-based development supported by Event-B has been extensively used in the domain of embedded and distributed systems design. For these domains timing analysis is of great importance. However, in its present form, Event-B does not have a built-in notion of time. The theory of refinement of timed transition systems has been studied, but a refinement-based design flow of these systems is weakly supported by industrial strength tools. In this paper, we focus on the refinement relation in the class of Uppaal Timed Automata and show how this relation is interrelated with the data refinement relation in Event-B. Using this interrelation we present a way how the Event-B and Uppaal tools can complement each other in a refinement-based design flow. The approach is demonstrated on a well-studied case-study, namely the IEEE 1394 tree identify protocol.

BibTeX entry:

@INBOOK{cVaTsBo16a,
  title = {Integrating Refinement-Based Methods for Developing Timed Systems},
  booktitle = {From Action Systems to Distributed Systems: The Refinement Approach},
  author = {Vain, Jüri and Tsiopoulos, Leonidas and Boström, Pontus},
  editor = {Petre, Luigia and Sekerinski, Emil},
  publisher = {Taylor & Francis},
  pages = {171 – 185},
  year = {2016},
  keywords = {Formal Methods, Real-Time Systems, Refinement, Verification, Modelling, Event-B, UPPAAL Timed Automata},
  ISSN = {978-0-335; 978-0-415; 978-0-84},
}

Belongs to TUCS Research Unit(s): Distributed Systems Laboratory (DS Lab), Embedded Systems Laboratory (ESLAB)

Publication Forum rating of this publication: level 2

Edit publication