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

被引：0

作者：

Zhao Jinfu ^{[1
]}

Zhang Hong ^{[1
]}

Wang Xuejing ^{[1
]}

机构：

[1] Beihang Univ, Sch Reliabil & Syst Engn, Sci & Technol Reliabil & Environm Engn Lab, Beijing 100191, Peoples R China

来源：

PROCEEDINGS OF THE 2015 INTERNATIONAL INDUSTRIAL INFORMATICS AND COMPUTER ENGINEERING CONFERENCE | 2015年

关键词：

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

D O I：

暂无

中图分类号：

TP [自动化技术、计算机技术];

学科分类号：

0812 ;

摘要：

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.

引用

页码：91 / 94

页数：4