Core Hybrid Event-B I: Single Hybrid Event-B machines. Banach, R., Butler, M., Qin, S., Verma, N., & Zhu, H. Science of Computer Programming, 105:92–123, July, 2015. ![Core Hybrid Event-B I: Single Hybrid Event-B machines [link]](https://bibbase.org/img/filetypes/link.svg "link")
Paper doi abstract bibtex Faced with the increasing need for correctly designed hybrid and cyber-physical systems today, the problem of including provision for continuously varying behaviour as well as the usual discrete changes of state is considered in the context of Event-B. An extension of Event-B called Hybrid Event-B is presented, that accommodates continuous behaviours (called pliant events) in between familiar discrete transitions (called mode events in this context). The continuous state change can be specified by a combination of indirect specification via ordinary differential equations, or direct specification via assignment of variables to values that depend on time, or indirect specification by demanding that behaviour obeys a time dependent predicate. The syntactic elements of the extension are discussed, and the semantics is described in terms of the properties of time dependent valuations of variables. Refinement is examined in detail, with reference to the notion of refinement inherited from discrete Event-B. A full suite of proof obligations is presented, covering all aspects of the new framework. A selection of examples and case studies is presented. A particular challenge — bearing in mind the desirability of conforming to existing intuitions about discrete Event-B, and the impact on tool support (as embodied in tools for discrete Event-B like Rodin) — is to design the whole framework so as to disturb as little as possible the existing structures for handling discrete Event-B.
@article{banach_core_2015,
title = {Core {Hybrid} {Event}-{B} {I}: {Single} {Hybrid} {Event}-{B} machines},
volume = {105},
issn = {0167-6423},
shorttitle = {Core {Hybrid} {Event}-{B} {I}},
url = {http://www.sciencedirect.com/science/article/pii/S0167642315000283},
doi = {10/f7f7cv},
abstract = {Faced with the increasing need for correctly designed hybrid and cyber-physical systems today, the problem of including provision for continuously varying behaviour as well as the usual discrete changes of state is considered in the context of Event-B. An extension of Event-B called Hybrid Event-B is presented, that accommodates continuous behaviours (called pliant events) in between familiar discrete transitions (called mode events in this context). The continuous state change can be specified by a combination of indirect specification via ordinary differential equations, or direct specification via assignment of variables to values that depend on time, or indirect specification by demanding that behaviour obeys a time dependent predicate. The syntactic elements of the extension are discussed, and the semantics is described in terms of the properties of time dependent valuations of variables. Refinement is examined in detail, with reference to the notion of refinement inherited from discrete Event-B. A full suite of proof obligations is presented, covering all aspects of the new framework. A selection of examples and case studies is presented. A particular challenge — bearing in mind the desirability of conforming to existing intuitions about discrete Event-B, and the impact on tool support (as embodied in tools for discrete Event-B like Rodin) — is to design the whole framework so as to disturb as little as possible the existing structures for handling discrete Event-B.},
language = {en},
urldate = {2020-09-30},
journal = {Science of Computer Programming},
author = {Banach, Richard and Butler, Michael and Qin, Shengchao and Verma, Nitika and Zhu, Huibiao},
month = jul,
year = {2015},
keywords = {Event-B, Formal development, Hybrid systems, Refinement},
pages = {92--123},
}
Downloads: 0
{"_id":"pzbQtozeFTskX2jpG","bibbaseid":"banach-butler-qin-verma-zhu-corehybrideventbisinglehybrideventbmachines-2015","author_short":["Banach, R.","Butler, M.","Qin, S.","Verma, N.","Zhu, H."],"bibdata":{"bibtype":"article","type":"article","title":"Core Hybrid Event-B I: Single Hybrid Event-B machines","volume":"105","issn":"0167-6423","shorttitle":"Core Hybrid Event-B I","url":"http://www.sciencedirect.com/science/article/pii/S0167642315000283","doi":"10/f7f7cv","abstract":"Faced with the increasing need for correctly designed hybrid and cyber-physical systems today, the problem of including provision for continuously varying behaviour as well as the usual discrete changes of state is considered in the context of Event-B. An extension of Event-B called Hybrid Event-B is presented, that accommodates continuous behaviours (called pliant events) in between familiar discrete transitions (called mode events in this context). The continuous state change can be specified by a combination of indirect specification via ordinary differential equations, or direct specification via assignment of variables to values that depend on time, or indirect specification by demanding that behaviour obeys a time dependent predicate. The syntactic elements of the extension are discussed, and the semantics is described in terms of the properties of time dependent valuations of variables. Refinement is examined in detail, with reference to the notion of refinement inherited from discrete Event-B. A full suite of proof obligations is presented, covering all aspects of the new framework. A selection of examples and case studies is presented. A particular challenge — bearing in mind the desirability of conforming to existing intuitions about discrete Event-B, and the impact on tool support (as embodied in tools for discrete Event-B like Rodin) — is to design the whole framework so as to disturb as little as possible the existing structures for handling discrete Event-B.","language":"en","urldate":"2020-09-30","journal":"Science of Computer Programming","author":[{"propositions":[],"lastnames":["Banach"],"firstnames":["Richard"],"suffixes":[]},{"propositions":[],"lastnames":["Butler"],"firstnames":["Michael"],"suffixes":[]},{"propositions":[],"lastnames":["Qin"],"firstnames":["Shengchao"],"suffixes":[]},{"propositions":[],"lastnames":["Verma"],"firstnames":["Nitika"],"suffixes":[]},{"propositions":[],"lastnames":["Zhu"],"firstnames":["Huibiao"],"suffixes":[]}],"month":"July","year":"2015","keywords":"Event-B, Formal development, Hybrid systems, Refinement","pages":"92–123","bibtex":"@article{banach_core_2015,\n\ttitle = {Core {Hybrid} {Event}-{B} {I}: {Single} {Hybrid} {Event}-{B} machines},\n\tvolume = {105},\n\tissn = {0167-6423},\n\tshorttitle = {Core {Hybrid} {Event}-{B} {I}},\n\turl = {http://www.sciencedirect.com/science/article/pii/S0167642315000283},\n\tdoi = {10/f7f7cv},\n\tabstract = {Faced with the increasing need for correctly designed hybrid and cyber-physical systems today, the problem of including provision for continuously varying behaviour as well as the usual discrete changes of state is considered in the context of Event-B. An extension of Event-B called Hybrid Event-B is presented, that accommodates continuous behaviours (called pliant events) in between familiar discrete transitions (called mode events in this context). The continuous state change can be specified by a combination of indirect specification via ordinary differential equations, or direct specification via assignment of variables to values that depend on time, or indirect specification by demanding that behaviour obeys a time dependent predicate. The syntactic elements of the extension are discussed, and the semantics is described in terms of the properties of time dependent valuations of variables. Refinement is examined in detail, with reference to the notion of refinement inherited from discrete Event-B. A full suite of proof obligations is presented, covering all aspects of the new framework. A selection of examples and case studies is presented. A particular challenge — bearing in mind the desirability of conforming to existing intuitions about discrete Event-B, and the impact on tool support (as embodied in tools for discrete Event-B like Rodin) — is to design the whole framework so as to disturb as little as possible the existing structures for handling discrete Event-B.},\n\tlanguage = {en},\n\turldate = {2020-09-30},\n\tjournal = {Science of Computer Programming},\n\tauthor = {Banach, Richard and Butler, Michael and Qin, Shengchao and Verma, Nitika and Zhu, Huibiao},\n\tmonth = jul,\n\tyear = {2015},\n\tkeywords = {Event-B, Formal development, Hybrid systems, Refinement},\n\tpages = {92--123},\n}\n\n","author_short":["Banach, R.","Butler, M.","Qin, S.","Verma, N.","Zhu, H."],"key":"banach_core_2015","id":"banach_core_2015","bibbaseid":"banach-butler-qin-verma-zhu-corehybrideventbisinglehybrideventbmachines-2015","role":"author","urls":{"Paper":"http://www.sciencedirect.com/science/article/pii/S0167642315000283"},"keyword":["Event-B","Formal development","Hybrid systems","Refinement"],"metadata":{"authorlinks":{}},"html":""},"bibtype":"article","biburl":"https://bibbase.org/zotero/SilverSylvester","dataSources":["YCBcQPneB9oxahSnp"],"keywords":["event-b","formal development","hybrid systems","refinement"],"search_terms":["core","hybrid","event","single","hybrid","event","machines","banach","butler","qin","verma","zhu"],"title":"Core Hybrid Event-B I: Single Hybrid Event-B machines","year":2015}