Pliant modalities in hybrid event-B

Richard Banach

doi:10.1007/978-3-642-39698-4_3

Pliant modalities in hybrid event-B

Richard Banach

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

Abstract

Hybrid Event-B includes provision for continuously varying behaviour as well as the usual discrete changes of state in the context of Event-B. As well as being able to specify hybrid behaviour in the usual way, using differential equations or continuous assignments for the continuous parts of the behaviour, looser ways of specifying behaviour at higher levels of abstraction are extremely useful. Although the need for such looser specification can be met using the logic of the formalism, certain metaphors (or patterns) occur so often, and are so useful in practice, that it is valuable to introduce special machinery into the specification language, to allow these frequently occurring patterns to be readily referred to. This paper introduces such machinery into Hybrid Event-B. © 2013 Springer-Verlag.

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	37-53
Number of pages	16
Volume	8051
ISBN (Print)	9783642396977
DOIs	https://doi.org/10.1007/978-3-642-39698-4_3
Publication status	Published - 2013
Event	Theories of Programming and Formal Methods: Essays Dedicated to Jifeng He on the Occasion of His 70th Birthday - Shanghai Duration: 1 Jul 2013 → …

Conference

Conference	Theories of Programming and Formal Methods: Essays Dedicated to Jifeng He on the Occasion of His 70th Birthday
City	Shanghai
Period	1/07/13 → …

Access to Document

10.1007/978-3-642-39698-4_3

Cite this

@inproceedings{b173b000c06a4afb990158b4d282151f,

title = "Pliant modalities in hybrid event-B",

abstract = "Hybrid Event-B includes provision for continuously varying behaviour as well as the usual discrete changes of state in the context of Event-B. As well as being able to specify hybrid behaviour in the usual way, using differential equations or continuous assignments for the continuous parts of the behaviour, looser ways of specifying behaviour at higher levels of abstraction are extremely useful. Although the need for such looser specification can be met using the logic of the formalism, certain metaphors (or patterns) occur so often, and are so useful in practice, that it is valuable to introduce special machinery into the specification language, to allow these frequently occurring patterns to be readily referred to. This paper introduces such machinery into Hybrid Event-B. {\textcopyright} 2013 Springer-Verlag.",

author = "Richard Banach",

year = "2013",

doi = "10.1007/978-3-642-39698-4\_3",

language = "English",

isbn = "9783642396977",

volume = "8051",

pages = "37--53",

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 = "Theories of Programming and Formal Methods: Essays Dedicated to Jifeng He on the Occasion of His 70th Birthday ; Conference date: 01-07-2013",

}

Banach, R 2013, Pliant modalities 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. 8051, Springer Nature, pp. 37-53, Theories of Programming and Formal Methods: Essays Dedicated to Jifeng He on the Occasion of His 70th Birthday, Shanghai, 1/07/13. https://doi.org/10.1007/978-3-642-39698-4_3

TY - GEN

T1 - Pliant modalities in hybrid event-B

AU - Banach, Richard

PY - 2013

Y1 - 2013

N2 - Hybrid Event-B includes provision for continuously varying behaviour as well as the usual discrete changes of state in the context of Event-B. As well as being able to specify hybrid behaviour in the usual way, using differential equations or continuous assignments for the continuous parts of the behaviour, looser ways of specifying behaviour at higher levels of abstraction are extremely useful. Although the need for such looser specification can be met using the logic of the formalism, certain metaphors (or patterns) occur so often, and are so useful in practice, that it is valuable to introduce special machinery into the specification language, to allow these frequently occurring patterns to be readily referred to. This paper introduces such machinery into Hybrid Event-B. © 2013 Springer-Verlag.

AB - Hybrid Event-B includes provision for continuously varying behaviour as well as the usual discrete changes of state in the context of Event-B. As well as being able to specify hybrid behaviour in the usual way, using differential equations or continuous assignments for the continuous parts of the behaviour, looser ways of specifying behaviour at higher levels of abstraction are extremely useful. Although the need for such looser specification can be met using the logic of the formalism, certain metaphors (or patterns) occur so often, and are so useful in practice, that it is valuable to introduce special machinery into the specification language, to allow these frequently occurring patterns to be readily referred to. This paper introduces such machinery into Hybrid Event-B. © 2013 Springer-Verlag.

U2 - 10.1007/978-3-642-39698-4_3

DO - 10.1007/978-3-642-39698-4_3

M3 - Conference contribution

SN - 9783642396977

VL - 8051

SP - 37

EP - 53

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 - Theories of Programming and Formal Methods: Essays Dedicated to Jifeng He on the Occasion of His 70th Birthday

Y2 - 1 July 2013

ER -

Pliant modalities in hybrid event-B

Abstract

Conference

Access to Document

Fingerprint

Cite this