id: 06086708
dt: a
an: 06086708
au: Berthing, Jesper; Boström, Pontus; Sere, Kaisa; Tsiopoulos, Leonidas;
    Vain, Jüri
ti: Refinement-based development of timed systems.
so: Derrick, John (ed.) et al., Integrated formal methods. 9th international
    conference, IFM 2012, Pisa, Italy, June 18‒21, 2012. Proceedings.
    Berlin: Springer (ISBN 978-3-642-30728-7/pbk). Lecture Notes in
    Computer Science 7321, 69-83 (2012).
py: 2012
pu: Berlin: Springer
la: EN
cc: 
ut: 
ci: 
li: doi:10.1007/978-3-642-30729-4_6
ab: Summary: 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 fragment of an industrial case
    study.
rv: