An Approach to Proving Proof Obligation of Hybrid Event B Based on Differential Invariants

Jie Liu; Jing Liu; Miaomiao Zhang; Haiying Sun; Xiaohong Chen; Dehui Du; Mingsong Chen

doi:10.1109/COMPSAC.2017.52

An Approach to Proving Proof Obligation of Hybrid Event B Based on Differential Invariants

Jie Liu, Jing Liu, Miaomiao Zhang, Haiying Sun, Xiaohong Chen, Dehui Du, Mingsong Chen

Software Engineering Institute

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

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.

Original language	English
Title of host publication	Proceedings - 2017 IEEE 41st Annual Computer Software and Applications Conference, COMPSAC 2017
Editors	Claudio Demartini, Thomas Conte, Motonori Nakamura, Chung-Horng Lung, Zhiyong Zhang, Kamrul Hasan, Sorel Reisman, Ling Liu, William Claycomb, Hiroki Takakura, Ji-Jiang Yang, Edmundo Tovar, Stelvio Cimato, Sheikh Iqbal Ahamed, Toyokazu Akiyama
Publisher	IEEE Computer Society
Pages	138-143
Number of pages	6
ISBN (Electronic)	9781538603673
DOIs	https://doi.org/10.1109/COMPSAC.2017.52
State	Published - 7 Sep 2017
Event	41st IEEE Annual Computer Software and Applications Conference, COMPSAC 2017 - Torino, Italy Duration: 4 Jul 2017 → 8 Jul 2017

Publication series

Name	Proceedings - International Computer Software and Applications Conference
Volume	1
ISSN (Print)	0730-3157

Conference

Conference	41st IEEE Annual Computer Software and Applications Conference, COMPSAC 2017
Country/Territory	Italy
City	Torino
Period	4/07/17 → 8/07/17

Keywords

Hybrid Event B
differential event
differential invariant
hybrid system
proof obligation

Access to Document

10.1109/COMPSAC.2017.52

Cite this

Liu, J., Liu, J., Zhang, M., Sun, H., Chen, X., Du, D., & Chen, M. (2017). An Approach to Proving Proof Obligation of Hybrid Event B Based on Differential Invariants. In C. Demartini, T. Conte, M. Nakamura, C.-H. Lung, Z. Zhang, K. Hasan, S. Reisman, L. Liu, W. Claycomb, H. Takakura, J.-J. Yang, E. Tovar, S. Cimato, S. I. Ahamed, & T. Akiyama (Eds.), Proceedings - 2017 IEEE 41st Annual Computer Software and Applications Conference, COMPSAC 2017 (pp. 138-143). Article 8029601 (Proceedings - International Computer Software and Applications Conference; Vol. 1). IEEE Computer Society. https://doi.org/10.1109/COMPSAC.2017.52

Liu, Jie ; Liu, Jing ; Zhang, Miaomiao et al. / An Approach to Proving Proof Obligation of Hybrid Event B Based on Differential Invariants. Proceedings - 2017 IEEE 41st Annual Computer Software and Applications Conference, COMPSAC 2017. editor / Claudio Demartini ; Thomas Conte ; Motonori Nakamura ; Chung-Horng Lung ; Zhiyong Zhang ; Kamrul Hasan ; Sorel Reisman ; Ling Liu ; William Claycomb ; Hiroki Takakura ; Ji-Jiang Yang ; Edmundo Tovar ; Stelvio Cimato ; Sheikh Iqbal Ahamed ; Toyokazu Akiyama. IEEE Computer Society, 2017. pp. 138-143 (Proceedings - International Computer Software and Applications Conference).

@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 = "美国",

}

Liu, J, Liu, J, Zhang, M, Sun, H, Chen, X, Du, D & Chen, M 2017, An Approach to Proving Proof Obligation of Hybrid Event B Based on Differential Invariants. in C Demartini, T Conte, M Nakamura, C-H Lung, Z Zhang, K Hasan, S Reisman, L Liu, W Claycomb, H Takakura, J-J Yang, E Tovar, S Cimato, SI Ahamed & T Akiyama (eds), Proceedings - 2017 IEEE 41st Annual Computer Software and Applications Conference, COMPSAC 2017., 8029601, Proceedings - International Computer Software and Applications Conference, vol. 1, IEEE Computer Society, pp. 138-143, 41st IEEE Annual Computer Software and Applications Conference, COMPSAC 2017, Torino, Italy, 4/07/17. https://doi.org/10.1109/COMPSAC.2017.52

An Approach to Proving Proof Obligation of Hybrid Event B Based on Differential Invariants. / Liu, Jie; Liu, Jing; Zhang, Miaomiao et al.
Proceedings - 2017 IEEE 41st Annual Computer Software and Applications Conference, COMPSAC 2017. ed. / Claudio Demartini; Thomas Conte; Motonori Nakamura; Chung-Horng Lung; Zhiyong Zhang; Kamrul Hasan; Sorel Reisman; Ling Liu; William Claycomb; Hiroki Takakura; Ji-Jiang Yang; Edmundo Tovar; Stelvio Cimato; Sheikh Iqbal Ahamed; Toyokazu Akiyama. IEEE Computer Society, 2017. p. 138-143 8029601 (Proceedings - International Computer Software and Applications Conference; Vol. 1).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - An Approach to Proving Proof Obligation of Hybrid Event B Based on Differential Invariants

AU - Liu, Jie

AU - Liu, Jing

AU - Zhang, Miaomiao

AU - Sun, Haiying

AU - Chen, Xiaohong

AU - Du, Dehui

AU - Chen, Mingsong

PY - 2017/9/7

Y1 - 2017/9/7

N2 - 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.

AB - 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.

KW - Hybrid Event B

KW - differential event

KW - differential invariant

KW - hybrid system

KW - proof obligation

UR - https://www.scopus.com/pages/publications/85031943502

U2 - 10.1109/COMPSAC.2017.52

DO - 10.1109/COMPSAC.2017.52

M3 - 会议稿件

AN - SCOPUS:85031943502

T3 - Proceedings - International Computer Software and Applications Conference

SP - 138

EP - 143

BT - Proceedings - 2017 IEEE 41st Annual Computer Software and Applications Conference, COMPSAC 2017

A2 - Demartini, Claudio

A2 - Conte, Thomas

A2 - Nakamura, Motonori

A2 - Lung, Chung-Horng

A2 - Zhang, Zhiyong

A2 - Hasan, Kamrul

A2 - Reisman, Sorel

A2 - Liu, Ling

A2 - Claycomb, William

A2 - Takakura, Hiroki

A2 - Yang, Ji-Jiang

A2 - Tovar, Edmundo

A2 - Cimato, Stelvio

A2 - Ahamed, Sheikh Iqbal

A2 - Akiyama, Toyokazu

PB - IEEE Computer Society

T2 - 41st IEEE Annual Computer Software and Applications Conference, COMPSAC 2017

Y2 - 4 July 2017 through 8 July 2017

ER -

Liu J, Liu J, Zhang M, Sun H, Chen X, Du D et al. An Approach to Proving Proof Obligation of Hybrid Event B Based on Differential Invariants. In Demartini C, Conte T, Nakamura M, Lung CH, Zhang Z, Hasan K, Reisman S, Liu L, Claycomb W, Takakura H, Yang JJ, Tovar E, Cimato S, Ahamed SI, Akiyama T, editors, Proceedings - 2017 IEEE 41st Annual Computer Software and Applications Conference, COMPSAC 2017. IEEE Computer Society. 2017. p. 138-143. 8029601. (Proceedings - International Computer Software and Applications Conference). doi: 10.1109/COMPSAC.2017.52

An Approach to Proving Proof Obligation of Hybrid Event B Based on Differential Invariants

Abstract

Publication series

Conference

Keywords

Access to Document

Other files and links

Fingerprint

Cite this