Verification of real-time properties based on Event-B models

DOI

10.2991/iiicec-15.2015.22How to use a DOI?

Keywords

real-time; verification; formal method; Event-B; UPPAAL

Abstract

A large number of dependable embedded systems have stringent real-time requirements, which cause real-time verification in modeling stage is desired. Event-B is a formal method used for system-level modeling and analysis, which is suitable for modeling high dependable software. Modeling real-time system in Event-B can ensure the reliability of system, while Event-B lacks real-time properties verification approaches at modeling stage. In this paper, one real-time property verification approaches for Event-B models assisted with UPPAAL is presented. Firstly, the Event-B models are transferred to UPPAAL models, and then UPPAAL checker is used to verify whether the UPPAAL models satisfied these terms.

Copyright

© 2015, the Authors. Published by Atlantis Press.

Open Access

This is an open access article distributed under the CC BY-NC license (http://creativecommons.org/licenses/by-nc/4.0/).

Download article (PDF)

TY  - CONF
AU  - Jinfu Zhao
AU  - Hong Zhang
AU  - Xuejing Wang
PY  - 2015/03
DA  - 2015/03
TI  - Verification of real-time properties based on Event-B models
BT  - Proceedings of the 2015 International Industrial Informatics and Computer Engineering Conference
PB  - Atlantis Press
SP  - 91
EP  - 94
SN  - 2352-538X
UR  - https://doi.org/10.2991/iiicec-15.2015.22
DO  - 10.2991/iiicec-15.2015.22
ID  - Zhao2015/03
ER  -