Abstract
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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
In sophisticated modern designs, active members are also found higher up the building, to counter vibration antinodes part way up a tall structure.
- 2.
If a mode event has an input, the semantics assumes that its value arrives at a time distinct from the previous mode event, ensuring part of (1) automatically.
- 3.
Idealizing a building by an equivalent SDOF system requires an assumption about its displaced shape and other details that are beyond the scope of the paper. The interested reader is directed to the methodology outlined by Kuramoto et al. [24], which is included in the current building design code used in Japan, as one example.
- 4.
The International Building Code (IBC) requires that drift be limited in typical buildings to 1–2% of the building’s height for reasons of both safety and functional performance.
- 5.
Of course, a more realistic model would contain modes for maintenance, and for other forms of partial running or of inactivity—to be used, presumably, only when the building is unoccupied.
- 6.
The issue is not a trivial one. HEB semantics is defined in terms of piecewise absolutely continuous functions [11]. But a delta function is not piecewise absolutely continuous, because, to be precise, it is not a function at all.
- 7.
In deriving this, we dropped a term \(-1\) from the RHS of (15).
- 8.
Mathematically, it is possible for both terms to have magnitude bigger than \(\varDelta {x}\), unless we take into account relevant upper bounds etc. and show that it is impossible. We will just assume that there is no such possibility in our problem space.
- 9.
The formal presentation of HEB [11] does not mention the anticipating status, since that is somewhat outside the main concerns there. But there is no reason to forbid it since it concerns purely structural matters.
- 10.
In reality, a sensor would send values in its own units, and scaling would be done as part of the controller’s job, but we avoid this so as to keep the controller calculation reasonably transparent.
- 11.
On a technical level, the building and actuator machines illustrate the pattern whereby synchronised mode events in different machines can instantaneously share values: one event uses an output variable and the others use an input variable with a complementary (CSP style) name.
- 12.
Note that this critically depends on insisting that intervals of pliant behaviour are left closed and right open.
- 13.
- 14.
Speaking realistically, in a genuine earthquake scenario, noise and experimental uncertainty are likely to be such that the differences between the ideal and conservative values of the constants vanish into insignificance. But it is worth checking that the mathematics confirms this.
- 15.
We can also regard all the previous models as each being in its own single machine project.
- 16.
In a contracting dynamics, nearby points are driven closer by the dynamics.
- 17.
The \(\tilde{1}\) refers to an \(L_1\) norm on the (instantaneous values of the) tilde variables.
- 18.
The form for i in range(n) is idiomatic Python for bounded iteration from 0 to \(n-1\) (inclusive).
- 19.
Being wooden, the Forbidden City’s buildings were less good at withstanding fire, and several structures have had to be rebuilt a number of times over the centuries because they had burnt down.
References
J. Earthq. Eng. Eng. Vib.
World Conferences on Earthquake Engineering
Abrial, J.R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press, Cambridge (2010)
Ahmed, N.: Dynamic Systems and Control With Applications. World Scientific, Singapore (2006)
Banach, R.: Formal refinement and partitioning of a fuel pump system for small aircraft in Hybrid Event-B. In: Bonsangue D. (eds.) Proceedings of IEEE TASE-16, pp. 65–72. IEEE (2016)
Banach, R.: Hemodialysis machine in Hybrid Event-B. In: Butler, S., Mashkoor B. (eds.) Proceedings of ABZ-16. LNCS, vol. 9675, pp. 376–393. Springer (2016)
Banach, R.: The landing gear system in multi-machine Hybrid Event-B. Int. J. Softw. Tools Tech. Transf. 19, 205–228 (2017)
Banach, R., Baugh, J.: Active earthquake control case study in Hybrid Event-B web site. http://www.cs.man.ac.uk/~banach/some.pubs/EarthquakeProtection/
Banach, R., Butler, M.: A Hybrid Event-B study of lane centering. In: Aiguier, B., Krob M. (eds.) Proceedings of CSDM-13, pp. 97–111. Springer (2013)
Banach, R., Butler, M.: Cruise control in Hybrid Event-B. In: Woodcock Z.L. (ed.) Proceedings of ICTAC-13. LNCS, vol. 8049, pp. 76–93. Springer (2013)
Banach, R., Butler, M., Qin, S., Verma, N., Zhu, H.: Core Hybrid Event-B I: single Hybrid Event-B machines. Sci. Comput. Program. 105, 92–123 (2015)
Banach, R., Butler, M., Qin, S., Zhu, H.: Core Hybrid Event-B II: multiple cooperating Hybrid Event-B machines. Sci. Comput. Program. 139, 1–35 (2017)
Banach, R., Jeske, C.: Retrenchment and refinement interworking: the tower theorems. Math. Struct. Comput. Sci. 25, 135–202 (2015)
Banach, R., Poppleton, M., Jeske, C., Stepney, S.: Engineering and theoretical underpinnings of retrenchment. Sci. Comput. Program. 67, 301–329 (2007)
Banach, R., Van Schaik, P., Verhulst, E.: Simulation and formal modelling of yaw control in a drive-by-wire application. In: Proceedings of FedCSIS IWCPS-15, pp. 731–742 (2015)
Baugh, J., Elseaidy, W.: Real-time software development with formal methods. J. Comput. Civ. Eng. 9, 73–86 (1995)
Buckle, I.: Passive control of structures for seismic loads. In: Proceedings of 12th World Conference on Earthquake Engineering. Paper No. 2825 (2000)
Chicone, C.: Ordinary Differential Equations with Applications, 2nd edn. Springer, New York (2006)
Chopra, A.: Dynamics of Structures: Theory and Applications to Earthquake Engineering, 4th edn. Pearson, Englewood Cliffs (2015)
Elseaidy, W., Baugh, J., Cleaveland, R.: Verification of an active control system using temporal process algebra. Eng. Comput. 12, 46–61 (1996)
Elseaidy, W., Cleaveland, R., Baugh, J.: Modeling and verifying active structural control systems. Sci. Comput. Program. 29, 99–122 (1997)
Gattulli, V., Lepidi, M., Potenza, F.: Seismic protection of frame structures via semi-active control: modelling and implementation issues. Earthq. Eng. Eng. Vib. 8, 627–645 (2009)
Gradshteyn, I., Ryzhik, I.: Table of Integrals Series and Products, 7th edn. Academic Press, New York (2007)
Kuramoto, H., Teshigawara, M., Okuzono, T., Koshika, N., Takayama, M., Hori, T.: Predicting the earthquake response of buildings using equivalent single degree of freedom system. In: Proceedings of 12th World Conference on Earthquake Engineering. Auckland, New Zealand. Paper No. 1039 (2000)
More4 TV: Secrets of China’s Forbidden City. UK Terrestrial TV Channel: More4. (24 July 2017)
Olver, F., Lozier, D., Boisvert, R., Clark, C.: NIST Handbook of Mathematical Functions. Cambridge University Press, Cambridge (2010)
Platzer, A.: Logical Analysis of Hybrid Systems: Proving Theorems for Complex Dynamics. Springer, Berlin (2010)
Popescu, I., Sireteanu, T., Mitu, A.: A comparative study of active and semi-active control of building seismic response. In: Proceedings of DGDS-09, pp. 172–177. Geometry Balkan Press (2010)
Prucz, Z., Soong, T., Reinhorn, A.: An analysis of pulse control for simple mechanical systems. J. Dyn. Syst. Meas. Control. 107, 123–131 (1985)
Retrenchment Homepage. http://www.cs.man.ac.uk/~banach/retrenchment
Rose, B., Baugh, J.: Parametric study of a pulse control algorithm with time delays. Technical report. CE-302-93, North Carolina State University Department of Civil Engineering (1993)
Sontag, E.: Mathematical Control Theory. Springer, New York (1998)
Soong, T.: Active Structural Control: Theory and Practice. Longman, Harlow (1990)
Soong, T., Chu, S., Reinhorn, A.: Active, Hybrid and Semi-Active Control: A Design and Implementation Handbook. Wiley, New York (2005)
Tabuada, P.: Verification and Control of Hybrid Systems: A Symbolic Approach. Springer, US (2009)
Walter, W.: Ordinary Differential Equations. Springer, Berlin (1998)
Wikipedia: Chinese architecture
Wikipedia: Dougong
Wikipedia: Duhamel’s integral
Wikipedia: Earthquake engineering
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2020 Springer Nature Switzerland AG
About this chapter
Cite this chapter
Banach, R., Baugh, J. (2020). A Simple Hybrid Event-B Model of an Active Control System for Earthquake Protection. In: Adamatzky, A., Kendon, V. (eds) From Astrophysics to Unconventional Computation. Emergence, Complexity and Computation, vol 35. Springer, Cham. https://doi.org/10.1007/978-3-030-15792-0_7
Download citation
DOI: https://doi.org/10.1007/978-3-030-15792-0_7
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-15791-3
Online ISBN: 978-3-030-15792-0
eBook Packages: Intelligent Technologies and RoboticsIntelligent Technologies and Robotics (R0)