A proof-based method of hybrid systems development using differential invariants

References

[1] Abrial J R. Modeling in Event-B: System and Software Engineering. Cambridge: Cambridge University Press, 2010

[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

[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

[4] Hallerstede S. On the purpose of Event-B proof obligations. Formal Aspects of Computing, 2011, 23(1): 133–150

[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

[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

[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

[9] Zhan N J, Wang S, Zhao H. Formal modelling, analysis and verification of hybrid systems. Lecture Notes in Computer Science, 2013, 207–281

[10] Platzer A. Logical analysis of hybrid systems. In: Proceedings of the International Workshop on Descriptional Complexity of Formal Systems. 2012: 43–49

RIGHTS & PERMISSIONS

Higher Education Press and Springer-Verlag GmbH Germany, part of Springer Nature