期刊论文、会议论文

Liu, Jing

英文

Proceedings - IEEE Computer Society's International Computer Software and Applications Conference

0730-3157

2017

1

138-143

41st IEEE Annual Computer Software and Applications Conference (COMPSAC)

Proceedings International Computer Software and Applications Conference

JUL 04-08, 2017

Torino, ITALY

[Liu, Jie;Liu, Jing;Sun, Haiying;Chen, Xiaohong;Du, Dehui;Chen, Mingsong] East China Normal Univ, Shanghai Key Lab Trustworthy Comp, Shanghai 200062, Peoples R China.^[Liu, Jie] Univ South China, Sch Comp Sci & Technol, Hengyang 421001, Peoples R China.^[Zhang, Miaomiao] Tongji Univ, Sch Software Engn, Shanghai 200062, Peoples R China.

IEEE, IEEE Comp Soc

Reisman, S Ahamed, SI Demartini, C Conte, T Liu, L Claycomb, W Nakamura, M Tovar, E Cimato, S Lung, CH Takakura, H Yang, JJ Akiyama, T Zhang, Z Hasan, K

345 E 47TH ST, NEW YORK, NY 10017 USA

IEEE

978-1-5386-0367-3

10.1109/COMPSAC.2017.52

NSFC Key ProjectNational Natural Science Foundation of China (NSFC) [61332008]; NSFCNational Natural Science Foundation of China (NSFC) [61572195]; Shanghai Project [SHEITC160306]; National Natural Science Foundation of ChinaNational Natural Science Foundation of China (NSFC) [61472279, 61472140, 61672230]; Natural Science Foundation of ShanghaiNatural Science Foundation of Shanghai [14ZR1412500]

本校为其他机构

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