Please wait a minute...

Frontiers of Computer Science

Front. Comput. Sci.    2018, Vol. 12 Issue (5) : 1026-1028     https://doi.org/10.1007/s11704-018-7213-y
LETTER |
A proof-based method of hybrid systems development using differential invariants
Jie LIU1,2, Jing LIU1(), Miaomiao ZHANG3(), Haiying SUN1, Xiaohong CHEN1, Dehui DU1, Mingsong CHEN1
1. Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, Shanghai 200062, China
2. School of Computer Science and Technology, University of South China, HengYang 421001, China
3. School of Software Engineering, Tongji University, Shanghai 201804, China
Download: PDF(217 KB)  
Export: BibTeX | EndNote | Reference Manager | ProCite | RefWorks
Corresponding Authors: Jing LIU,Miaomiao ZHANG   
Just Accepted Date: 27 July 2018   Online First Date: 04 September 2018    Issue Date: 21 September 2018
 Cite this article:   
Jie LIU,Jing LIU,Miaomiao ZHANG, et al. A proof-based method of hybrid systems development using differential invariants[J]. Front. Comput. Sci., 2018, 12(5): 1026-1028.
 URL:  
http://journal.hep.com.cn/fcs/EN/10.1007/s11704-018-7213-y
http://journal.hep.com.cn/fcs/EN/Y2018/V12/I5/1026
Service
E-mail this article
E-mail Alert
RSS
Articles by authors
Jie LIU
Jing LIU
Miaomiao ZHANG
Haiying SUN
Xiaohong CHEN
Dehui DU
Mingsong CHEN
1 Abrial J R. Modeling in Event-B: System and Software Engineering. Cambridge: Cambridge University Press, 2010
https://doi.org/10.1017/CBO9781139195881
2 Su W, Abrial J R, Zhu H. Formalizing hybrid systems with Event-B and the rodin platform. Science of Computer Programming, 2014, 94(4): 164–202
https://doi.org/10.1016/j.scico.2014.04.015
3 Banach R, Butler M, Qin S, Verma N, Zhu H. Core hybrid Event-B I: single hybrid Event-B machines. Science of Computer Programming, 2015, 105(7): 92–123
https://doi.org/10.1016/j.scico.2015.02.003
4 Hallerstede S. On the purpose of Event-B proof obligations. Formal Aspects of Computing, 2011, 23(1): 133–150
https://doi.org/10.1007/s00165-009-0138-3
5 Bu L, Xie D B. Formal verification of hybrid system. Journal of Software, 2014, 25(2): 219–233
6 Ratschan S, She Z. Safety verification of hybrid systems by constraint propagation based abstraction refinement. Lecture Notes in Computer Science, 2007, 3414: 573–589
https://doi.org/10.1007/978-3-540-31954-2_37
7 Zheng X, She Z, Liang Q, Li M. Inner approximations of domains of attraction for a class of switched systems by computing lyapunovlike functions. International Journal of Robust and Nonlinear Control, 2018, 4(1): 2191–2208
https://doi.org/10.1002/rnc.4010
8 She Z, Xue B. Computing an invariance kernel with target by computing lyapunov-like functions. IET Control Theory and Applications, 2013, 7(15): 1932–1940
https://doi.org/10.1049/iet-cta.2013.0275
9 Zhan N J, Wang S, Zhao H. Formal modelling, analysis and verification of hybrid systems. Lecture Notes in Computer Science, 2013, 207–281
https://doi.org/10.1007/978-3-642-39721-9_5
10 Platzer A. Logical analysis of hybrid systems. In: Proceedings of the International Workshop on Descriptional Complexity of Formal Systems. 2012: 43–49
https://doi.org/10.1007/978-3-642-31623-4_3
Viewed
Full text


Abstract

Cited

  Shared   
  Discussed