{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,4]],"date-time":"2022-04-04T15:41:48Z","timestamp":1649086908005},"reference-count":10,"publisher":"Springer Science and Business Media LLC","issue":"5","license":[{"start":{"date-parts":[[2018,9,5]],"date-time":"2018-09-05T00:00:00Z","timestamp":1536105600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Front. Comput. Sci."],"published-print":{"date-parts":[[2018,10]]},"DOI":"10.1007\/s11704-018-7213-y","type":"journal-article","created":{"date-parts":[[2018,9,5]],"date-time":"2018-09-05T10:11:37Z","timestamp":1536142297000},"page":"1026-1028","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["A proof-based method of hybrid systems development using differential invariants"],"prefix":"10.1007","volume":"12","author":[{"given":"Jie","family":"Liu","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jing","family":"Liu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Miaomiao","family":"Zhang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Haiying","family":"Sun","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xiaohong","family":"Chen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dehui","family":"Du","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mingsong","family":"Chen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,9,5]]},"reference":[{"key":"7213_CR1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139195881","volume-title":"Modeling in Event-B: System and Software Engineering","author":"J R Abrial","year":"2010","unstructured":"Abrial J R. Modeling in Event-B: System and Software Engineering. Cambridge: Cambridge University Press, 2010"},{"issue":"4","key":"7213_CR2","doi-asserted-by":"publisher","first-page":"164","DOI":"10.1016\/j.scico.2014.04.015","volume":"94","author":"W Su","year":"2014","unstructured":"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\u2013202","journal-title":"Science of Computer Programming"},{"issue":"7","key":"7213_CR3","doi-asserted-by":"publisher","first-page":"92","DOI":"10.1016\/j.scico.2015.02.003","volume":"105","author":"R Banach","year":"2015","unstructured":"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\u2013123","journal-title":"Science of Computer Programming"},{"issue":"1","key":"7213_CR4","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1007\/s00165-009-0138-3","volume":"23","author":"S Hallerstede","year":"2011","unstructured":"Hallerstede S. On the purpose of Event-B proof obligations. Formal Aspects of Computing, 2011, 23(1): 133\u2013150","journal-title":"Formal Aspects of Computing"},{"issue":"2","key":"7213_CR5","first-page":"219","volume":"25","author":"L Bu","year":"2014","unstructured":"Bu L, Xie D B. Formal verification of hybrid system. Journal of Software, 2014, 25(2): 219\u2013233","journal-title":"Journal of Software"},{"key":"7213_CR6","doi-asserted-by":"publisher","first-page":"573","DOI":"10.1007\/978-3-540-31954-2_37","volume":"3414","author":"S Ratschan","year":"2007","unstructured":"Ratschan S, She Z. Safety verification of hybrid systems by constraint propagation based abstraction refinement. Lecture Notes in Computer Science, 2007, 3414: 573\u2013589","journal-title":"Lecture Notes in Computer Science"},{"issue":"1","key":"7213_CR7","doi-asserted-by":"publisher","first-page":"2191","DOI":"10.1002\/rnc.4010","volume":"4","author":"X Zheng","year":"2018","unstructured":"Zheng X, She Z, Liang Q, Li M. Inner approximations of domains of attraction for a class of switched systems by computing lyapunov-like functions. International Journal of Robust and Nonlinear Control, 2018, 4(1): 2191\u20132208","journal-title":"International Journal of Robust and Nonlinear Control"},{"issue":"15","key":"7213_CR8","doi-asserted-by":"publisher","first-page":"1932","DOI":"10.1049\/iet-cta.2013.0275","volume":"7","author":"Z She","year":"2013","unstructured":"She Z, Xue B. Computing an invariance kernel with target by computing lyapunov-like functions. IET Control Theory and Applications, 2013, 7(15): 1932\u20131940","journal-title":"IET Control Theory and Applications"},{"key":"7213_CR9","first-page":"207","volume-title":"Lecture Notes in Computer Science","author":"N J Zhan","year":"2013","unstructured":"Zhan N J, Wang S, Zhao H. Formal modelling, analysis and verification of hybrid systems. Lecture Notes in Computer Science, 2013, 207\u2013281"},{"key":"7213_CR10","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1007\/978-3-642-31623-4_3","volume-title":"Proceedings of the International Workshop on Descriptional Complexity of Formal Systems","author":"A Platzer","year":"2012","unstructured":"Platzer A. Logical analysis of hybrid systems. In: Proceedings of the International Workshop on Descriptional Complexity of Formal Systems. 2012: 43\u201349"}],"container-title":["Frontiers of Computer Science"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11704-018-7213-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11704-018-7213-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11704-018-7213-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,4]],"date-time":"2019-09-04T23:13:19Z","timestamp":1567638799000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11704-018-7213-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,9,5]]},"references-count":10,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2018,10]]}},"alternative-id":["7213"],"URL":"https:\/\/doi.org\/10.1007\/s11704-018-7213-y","relation":{},"ISSN":["2095-2228","2095-2236"],"issn-type":[{"value":"2095-2228","type":"print"},{"value":"2095-2236","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,9,5]]},"assertion":[{"value":"19 June 2017","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"22 June 2018","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"5 September 2018","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}