Name
Abstract | ||
|---|---|---|
In this paper, we present Hybrid Event B, a formal language for modeling hybrid systems. Specifically, Hybrid Event B is an extension of Event B associating with differential dynamic logic. The main contribution of this paper is that we give the definition of a differential event in Hybrid Event B, which makes it possible using differential dynamic logic in modeling continuous dynamical systems and discrete dynamical systems. In addition, we show the proof obligations of each refinements on differential events, which supports the stepwise development of refinement. We also show the transformer semantics of the differential events and the weakest precondition refinement approach applied to hybrid systems, both of which support our stepwise development of hybrid systems. |
Year | DOI | Venue |
|---|---|---|
2014 | 10.1016/j.entcs.2014.12.002 | Electronic Notes in Theoretical Computer Science |
Keywords | Field | DocType |
Event B,differential dynamic logic,continuous refinement,hybrid systems | Predicate transformer semantics,Discrete mathematics,Formal language,Computer science,Theoretical computer science,Dynamical systems theory,Dynamic logic (digital electronics),Stepwise development,Hybrid system,Semantics | Journal |
Volume | Issue | ISSN |
309 | C | 1571-0661 |
Citations | PageRank | References |
1 | 0.36 | 12 |
Authors | ||
2 | ||