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

Modelling Critical Systems with Time Constraints in Event-B

Faezeh Siavashi, Marina Waldén, Leonidas Tsiopoulos, Jüri Vain, Modelling Critical Systems with Time Constraints in Event-B. In: Tarmo Uustalu, Jüri Vain (Eds.), Proceedings of the 25th Nordic Workshop on Programming Theory, NWPT '13, 1–3, Tallin University of Technology, 2013.

Abstract:

Developing real-time systems is an important concern in computer engineering. Applying formal methods is a rigorous solution to verify the reliability and correctness of such systems. By using the Event-B formal language, we modelled an industrial case study verifying the safety functioning of shutting down a real-time system. The shutdown is integrated with the timing constraints, which are not sufficiently supported in Event-B. This paper emphasizes on how real-time features can be expressed and verified in Event-B. The solution is illustrated with an industrial case study. We investigated two timing constraint patterns and their refinements in Uppaal and transformed them to Event-B. The proof obligations concerning the modelling of time are preserved.

Files:

Abstract in PDF-format

BibTeX entry:

@INPROCEEDINGS{inpSiWaTsVa13a,
  title = {Modelling Critical Systems with Time Constraints in Event-B},
  booktitle = {Proceedings of the 25th Nordic Workshop on Programming Theory, NWPT '13},
  author = {Siavashi, Faezeh and Waldén, Marina and Tsiopoulos, Leonidas and Vain, Jüri},
  editor = {Uustalu, Tarmo and Vain, Jüri},
  publisher = {Tallin University of Technology},
  pages = {1–3},
  year = {2013},
}

Belongs to TUCS Research Unit(s): Distributed Systems Laboratory (DS Lab), Software Engineering Laboratory (SE Lab)

Edit publication