Proceedings of the 2015 International Industrial Informatics and Computer Engineering Conference

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

Authors
Jinfu Zhao, Hong Zhang, Xuejing Wang
Corresponding Author
Jinfu Zhao
Available Online March 2015.
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)

Volume Title
Proceedings of the 2015 International Industrial Informatics and Computer Engineering Conference
Series
Advances in Computer Science Research
Publication Date
March 2015
ISBN
978-94-62520-54-7
ISSN
2352-538X
DOI
10.2991/iiicec-15.2015.22How to use a DOI?
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/).

Cite this article

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  -