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

  • Richard BanachEmail author
  • John Baugh
Part of the Emergence, Complexity and Computation book series (ECC, volume 35)


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.


  1. 1.
    J. Earthq. Eng. Eng. Vib.Google Scholar
  2. 2.
    World Conferences on Earthquake EngineeringGoogle Scholar
  3. 3.
    Abrial, J.R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press, Cambridge (2010)CrossRefGoogle Scholar
  4. 4.
    Ahmed, N.: Dynamic Systems and Control With Applications. World Scientific, Singapore (2006)CrossRefGoogle Scholar
  5. 5.
    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)Google Scholar
  6. 6.
    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)Google Scholar
  7. 7.
    Banach, R.: The landing gear system in multi-machine Hybrid Event-B. Int. J. Softw. Tools Tech. Transf. 19, 205–228 (2017)CrossRefGoogle Scholar
  8. 8.
    Banach, R., Baugh, J.: Active earthquake control case study in Hybrid Event-B web site.
  9. 9.
    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)Google Scholar
  10. 10.
    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)Google Scholar
  11. 11.
    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)CrossRefGoogle Scholar
  12. 12.
    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)CrossRefGoogle Scholar
  13. 13.
    Banach, R., Jeske, C.: Retrenchment and refinement interworking: the tower theorems. Math. Struct. Comput. Sci. 25, 135–202 (2015)MathSciNetCrossRefGoogle Scholar
  14. 14.
    Banach, R., Poppleton, M., Jeske, C., Stepney, S.: Engineering and theoretical underpinnings of retrenchment. Sci. Comput. Program. 67, 301–329 (2007)MathSciNetCrossRefGoogle Scholar
  15. 15.
    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)Google Scholar
  16. 16.
    Baugh, J., Elseaidy, W.: Real-time software development with formal methods. J. Comput. Civ. Eng. 9, 73–86 (1995)CrossRefGoogle Scholar
  17. 17.
    Buckle, I.: Passive control of structures for seismic loads. In: Proceedings of 12th World Conference on Earthquake Engineering. Paper No. 2825 (2000)Google Scholar
  18. 18.
    Chicone, C.: Ordinary Differential Equations with Applications, 2nd edn. Springer, New York (2006)zbMATHGoogle Scholar
  19. 19.
    Chopra, A.: Dynamics of Structures: Theory and Applications to Earthquake Engineering, 4th edn. Pearson, Englewood Cliffs (2015)Google Scholar
  20. 20.
    Elseaidy, W., Baugh, J., Cleaveland, R.: Verification of an active control system using temporal process algebra. Eng. Comput. 12, 46–61 (1996)CrossRefGoogle Scholar
  21. 21.
    Elseaidy, W., Cleaveland, R., Baugh, J.: Modeling and verifying active structural control systems. Sci. Comput. Program. 29, 99–122 (1997)CrossRefGoogle Scholar
  22. 22.
    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)CrossRefGoogle Scholar
  23. 23.
    Gradshteyn, I., Ryzhik, I.: Table of Integrals Series and Products, 7th edn. Academic Press, New York (2007)zbMATHGoogle Scholar
  24. 24.
    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)Google Scholar
  25. 25.
    More4 TV: Secrets of China’s Forbidden City. UK Terrestrial TV Channel: More4. (24 July 2017)Google Scholar
  26. 26.
    Olver, F., Lozier, D., Boisvert, R., Clark, C.: NIST Handbook of Mathematical Functions. Cambridge University Press, Cambridge (2010)zbMATHGoogle Scholar
  27. 27.
    Platzer, A.: Logical Analysis of Hybrid Systems: Proving Theorems for Complex Dynamics. Springer, Berlin (2010)CrossRefGoogle Scholar
  28. 28.
    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)Google Scholar
  29. 29.
    Prucz, Z., Soong, T., Reinhorn, A.: An analysis of pulse control for simple mechanical systems. J. Dyn. Syst. Meas. Control. 107, 123–131 (1985)CrossRefGoogle Scholar
  30. 30.
  31. 31.
    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)Google Scholar
  32. 32.
    Sontag, E.: Mathematical Control Theory. Springer, New York (1998)CrossRefGoogle Scholar
  33. 33.
    Soong, T.: Active Structural Control: Theory and Practice. Longman, Harlow (1990)Google Scholar
  34. 34.
    Soong, T., Chu, S., Reinhorn, A.: Active, Hybrid and Semi-Active Control: A Design and Implementation Handbook. Wiley, New York (2005)Google Scholar
  35. 35.
    Tabuada, P.: Verification and Control of Hybrid Systems: A Symbolic Approach. Springer, US (2009)CrossRefGoogle Scholar
  36. 36.
    Walter, W.: Ordinary Differential Equations. Springer, Berlin (1998)CrossRefGoogle Scholar
  37. 37.
    Wikipedia: Chinese architectureGoogle Scholar
  38. 38.
    Wikipedia: DougongGoogle Scholar
  39. 39.
    Wikipedia: Duhamel’s integralGoogle Scholar
  40. 40.
    Wikipedia: Earthquake engineeringGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2020

Authors and Affiliations

  1. 1.School of Computer ScienceUniversity of ManchesterManchesterUK
  2. 2.Department of Civil, Construction, and Environmental EngineeringNorth Carolina State UniversityRaleighUSA

Personalised recommendations