Refinement-Based Development of Timed Systems

  • Jesper Berthing
  • Pontus Boström
  • Kaisa Sere
  • Leonidas Tsiopoulos
  • Jüri Vain
Part of the Lecture Notes in Computer Science book series (LNCS, volume 7321)


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.


Model Check Label Transition System Proof Obligation International Electrotechnical Commission Safety Function 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Abrial, J.-R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press (2010)Google Scholar
  2. 2.
    Behrmann, G., David, A., Larsen, K.G.: A Tutorial on Uppaal. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol. 3185, pp. 200–236. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  3. 3.
    Bouyer, P., Laroussinie, F., Reynier, P.-A.: Diagonal Constraints in Timed Automata: Forward Analysis of Timed Systems. In: Pettersson, P., Yi, W. (eds.) FORMATS 2005. LNCS, vol. 3829, pp. 112–126. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  4. 4.
    Cansell, D., Méry, D., Rehm, J.: Time Constraint Patterns for Event B Development. In: Julliand, J., Kouchnarenko, O. (eds.) B 2007. LNCS, vol. 4355, pp. 140–154. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  5. 5.
    Chaudhari, D.L., Damani, O.P.: Generating hierarchical state based representation from Event-B models. In: Proceedings of the B 2011 Workshop. ENTCS, vol. 280 (2011)Google Scholar
  6. 6.
    Chimisliu, V., Wotawa, F.: Abstracting timing information in UML state charts via temporal ordering and LOTOS. In: AST 2011, pp. 8–14. ACM (2011)Google Scholar
  7. 7.
    David, A., Larsen, K.G., Legay, A., Nyman, U., Wasowski, A.: Timed I/O Automata: A complete specification theory for real-time systems. In: HSCC 2010. ACM (2011)Google Scholar
  8. 8.
    Dierks, H., Kupferschmid, S., Larsen, K.G.: Automatic Abstraction Refinement for Timed Automata. In: Raskin, J.-F., Thiagarajan, P.S. (eds.) FORMATS 2007. LNCS, vol. 4763, pp. 114–129. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  9. 9.
    International Electrotechnical Commission (IEC). IEC 61508-6: Functional safety of electrical/electronic/programmable electronic safety-related systems, 2nd edn. (2010)Google Scholar
  10. 10.
    Iliasov, A., Laibinis, L., Troubitsyna, E., Romanovsky, A., Latvala, T.: Augmenting Event-B modelling with real-time verification. Technical Report 1006, TUCS (2011)Google Scholar
  11. 11.
    Lamport, L.: Real-Time Model Checking Is Really Simple. In: Borrione, D., Paul, W. (eds.) CHARME 2005. LNCS, vol. 3725, pp. 162–175. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  12. 12.
    Lynch, N., Vaandrager, F.: Forward and backward simulations - Part II: Timing-Based systems. Information and Computation 128 (1995)Google Scholar
  13. 13.
    Sarshogh, M.R., Butler, M.: Specification and refinement of discrete timing properties in Event-B. Technical report, Electronic and Computer Science, University of Southampton (2011)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2012

Authors and Affiliations

  • Jesper Berthing
    • 1
  • Pontus Boström
    • 2
  • Kaisa Sere
    • 2
  • Leonidas Tsiopoulos
    • 2
  • Jüri Vain
    • 3
  1. 1.Danfoss Power Electronics A/SDenmark
  2. 2.Åbo Akademi UniversityFinland
  3. 3.Tallinn University of TechnologyEstonia

Personalised recommendations