Cruise control in hybrid event-B

Richard Banach; Michael Butler

doi:10.1007/978-3-642-39718-9-5

Cruise control in hybrid event-B

Research output: Chapter in Book/Conference proceeding › Conference contribution › peer-review

Abstract

A case study on automotive cruise control originally done in (conventional, discrete) Event-B is reexamined in Hybrid Event-B (an extension of Event-B that includes provision for continuously varying behaviour as well as the usual discrete changes of state). A significant case study such as this has various benefits. It can confirm that the Hybrid Event-B design allows appropriately fluent application level modelling (as is needed for serious industrial use). It also permits a critical comparison to be made between purely discrete and genuinely hybrid modelling. The latter enables application requirements to be covered in a more natural way. It also enables some inconvenient modelling metaphors to be eliminated. © 2013 Springer-Verlag Berlin Heidelberg.

Original language	English
Title of host publication	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)\|Lect. Notes Comput. Sci.
Publisher	Springer Nature
Pages	76-93
Number of pages	17
Volume	8049
ISBN (Print)	9783642397172
DOIs	https://doi.org/10.1007/978-3-642-39718-9-5
Publication status	Published - 2013
Event	10th International Colloquium on Theoretical Aspects of Computing, ICTAC 2013 - Shanghai Duration: 1 Jul 2013 → …

Conference

Conference	10th International Colloquium on Theoretical Aspects of Computing, ICTAC 2013
City	Shanghai
Period	1/07/13 → …

Access to Document

10.1007/978-3-642-39718-9-5

Cite this

@inproceedings{e2ff1afafaf0426083271e9b5d1ca21d,

title = "Cruise control in hybrid event-B",

abstract = "A case study on automotive cruise control originally done in (conventional, discrete) Event-B is reexamined in Hybrid Event-B (an extension of Event-B that includes provision for continuously varying behaviour as well as the usual discrete changes of state). A significant case study such as this has various benefits. It can confirm that the Hybrid Event-B design allows appropriately fluent application level modelling (as is needed for serious industrial use). It also permits a critical comparison to be made between purely discrete and genuinely hybrid modelling. The latter enables application requirements to be covered in a more natural way. It also enables some inconvenient modelling metaphors to be eliminated. {\textcopyright} 2013 Springer-Verlag Berlin Heidelberg.",

author = "Richard Banach and Michael Butler",

year = "2013",

doi = "10.1007/978-3-642-39718-9-5",

language = "English",

isbn = "9783642397172",

volume = "8049",

pages = "76--93",

booktitle = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)|Lect. Notes Comput. Sci.",

publisher = "Springer Nature",

address = "United States",

note = "10th International Colloquium on Theoretical Aspects of Computing, ICTAC 2013 ; Conference date: 01-07-2013",

}

Banach, R & Butler, M 2013, Cruise control in hybrid event-B. in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)|Lect. Notes Comput. Sci.. vol. 8049, Springer Nature, pp. 76-93, 10th International Colloquium on Theoretical Aspects of Computing, ICTAC 2013, Shanghai, 1/07/13. https://doi.org/10.1007/978-3-642-39718-9-5

TY - GEN

T1 - Cruise control in hybrid event-B

AU - Banach, Richard

AU - Butler, Michael

PY - 2013

Y1 - 2013

N2 - A case study on automotive cruise control originally done in (conventional, discrete) Event-B is reexamined in Hybrid Event-B (an extension of Event-B that includes provision for continuously varying behaviour as well as the usual discrete changes of state). A significant case study such as this has various benefits. It can confirm that the Hybrid Event-B design allows appropriately fluent application level modelling (as is needed for serious industrial use). It also permits a critical comparison to be made between purely discrete and genuinely hybrid modelling. The latter enables application requirements to be covered in a more natural way. It also enables some inconvenient modelling metaphors to be eliminated. © 2013 Springer-Verlag Berlin Heidelberg.

AB - A case study on automotive cruise control originally done in (conventional, discrete) Event-B is reexamined in Hybrid Event-B (an extension of Event-B that includes provision for continuously varying behaviour as well as the usual discrete changes of state). A significant case study such as this has various benefits. It can confirm that the Hybrid Event-B design allows appropriately fluent application level modelling (as is needed for serious industrial use). It also permits a critical comparison to be made between purely discrete and genuinely hybrid modelling. The latter enables application requirements to be covered in a more natural way. It also enables some inconvenient modelling metaphors to be eliminated. © 2013 Springer-Verlag Berlin Heidelberg.

U2 - 10.1007/978-3-642-39718-9-5

DO - 10.1007/978-3-642-39718-9-5

M3 - Conference contribution

SN - 9783642397172

VL - 8049

SP - 76

EP - 93

BT - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)|Lect. Notes Comput. Sci.

PB - Springer Nature

T2 - 10th International Colloquium on Theoretical Aspects of Computing, ICTAC 2013

Y2 - 1 July 2013

ER -

Cruise control in hybrid event-B

Abstract

Conference

Access to Document

Fingerprint

Cite this