A Simple Hybrid Event-B Model of an Active Control System for Earthquake Protection

Richard Banach, John Baugh

Research output: Chapter in Book/Report/Conference proceedingChapterpeer-review


In earthquake-prone zones of the world, severe damage to buildings and life endangering harm to people pose a major risk when severe earthquakes happen.
In recent decades, active and passive measures to prevent building damage have been designed and deployed. A simple model of an active damage prevention
system, founded on earlier work, is investigated from a model based formal development perspective, using Hybrid Event-B. The non-trivial physical behaviour in the model is readily captured within the formalism. However, when the usual approximation and discretization techniques from engineering and applied mathematics are used, the rather brittle refinement techniques used in model based formal development start to break down. Despite this, the model developed stands up well when compared via simulation with a standard
approach. The requirements of a richer formal development framework, better able to cope with applications exhibiting non-trivial physical elements are discussed.
Original languageEnglish
Title of host publicationAstrophysics to Unconventional Computing
Subtitle of host publicationEssays presented to Susan Stepney on the occasion of her 60th birthday
Publication statusPublished - 17 Apr 2019

Publication series

NameEmergence, Complexity and Computation
ISSN (Electronic)2194-7287


Dive into the research topics of 'A Simple Hybrid Event-B Model of an Active Control System for Earthquake Protection'. Together they form a unique fingerprint.

Cite this