@inproceedings{4226a254768e4fd18e4a319178742d7d,
title = "An Approach to Proving Proof Obligation of Hybrid Event B Based on Differential Invariants",
abstract = "For modelling hybrid systems, we have extended Event B based on its framework with the differential event. The differential event describes continuous behaviors of hybrid systems by differential equations and evolution constraint, whose proof obligations provide dynamical properties of a model. In order to ensure the safety and reliability of a model, proof obligations should be proved. It is difficult to prove proof obligation in state space, because there is no a complete method to solve differential equations in the field of mathematics. Thus we proposed an approach to proving proof obligation based on differential invariants. It is to avoid uncontrollable computation on solving differential equation. The main result is that we prove some theorems for proving proof obligations involving differential events within the framework of refinement calculus. Lastly, through the case of the Train Control System, we further show that the approach is well suited.",
keywords = "Hybrid Event B, differential event, differential invariant, hybrid system, proof obligation",
author = "Jie Liu and Jing Liu and Miaomiao Zhang and Haiying Sun and Xiaohong Chen and Dehui Du and Mingsong Chen",
note = "Publisher Copyright: {\textcopyright} 2017 IEEE.; 41st IEEE Annual Computer Software and Applications Conference, COMPSAC 2017 ; Conference date: 04-07-2017 Through 08-07-2017",
year = "2017",
month = sep,
day = "7",
doi = "10.1109/COMPSAC.2017.52",
language = "英语",
series = "Proceedings - International Computer Software and Applications Conference",
publisher = "IEEE Computer Society",
pages = "138--143",
editor = "Claudio Demartini and Thomas Conte and Motonori Nakamura and Chung-Horng Lung and Zhiyong Zhang and Kamrul Hasan and Sorel Reisman and Ling Liu and William Claycomb and Hiroki Takakura and Ji-Jiang Yang and Edmundo Tovar and Stelvio Cimato and Ahamed, \{Sheikh Iqbal\} and Toyokazu Akiyama",
booktitle = "Proceedings - 2017 IEEE 41st Annual Computer Software and Applications Conference, COMPSAC 2017",
address = "美国",
}