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

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.