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

Refinement-Based Development of Timed Systems

Jesper Berthing, Pontus Boström, Kaisa Sere, Leonidas Tsiopoulos, Jüri Vain, Refinement-Based Development of Timed Systems. In: Diego Latella, Helen Treharne (Eds.), 9th International Conference on Integrated Formal Methods (iFM 2012), Lecture Notes in Computer Science 7321, 69–84, Springer, Heidelberg, 2012.

Abstract:

Renement-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 renement of timed transition systems has been studied, but a renement-based design ow of these systems is weakly supported by industrial strength tools. In this paper, we focus on the renement relation in the class of Uppaal Timed Automata and show how this relation is interrelated with the data renement relation in Event-B. Using this interrelation we present a way how the Event-B and Uppaal tools can complement each other in a renement-based design ow. The approach is demonstrated on a fragment of an industrial case study.

BibTeX entry:

@INPROCEEDINGS{inpBeBoSeTsVa12a,
  title = {Refinement-Based Development of Timed Systems},
  booktitle = {9th International Conference on Integrated Formal Methods (iFM 2012)},
  author = {Berthing, Jesper and Boström, Pontus and Sere, Kaisa and Tsiopoulos, Leonidas and Vain, Jüri},
  volume = {7321},
  series = {Lecture Notes in Computer Science},
  editor = {Latella, Diego and Treharne, Helen},
  publisher = {Springer, Heidelberg},
  pages = {69–84},
  year = {2012},
}

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

Publication Forum rating of this publication: level 1

Edit publication