Verification of real-time properties based on Event-B models
Jinfu Zhao, Hong Zhang, Xuejing Wang · Advances in computer science research · 2015
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.