Acknowledgements This paper is partially supported by the funding under National Key Research and Development Project (2017YFB1001800), the NSFC Key Project (61332008) and NSFC (61572195). The Shanghai Trustworthy Computing Key Lab is supported by Shanghai Project (SHEITC160306). The third author would like to thanks the support of NSFC (61472279).
机构署名：
本校为其他机构
院系归属：
计算机科学与技术学院
摘要：
Event-B is a widely applied and proof-based language for incremental development via refinement [1]. Hybrid systems exhibit hybrid characteristics of discrete control and real-time continuous behaviors. However, Event-B is a discrete modeling language. It does not support the development of hybrid systems. So, the researchers are currently trying to make the extension of Event-B for th...
