The Use of Automated Theory Formation in Support of Hazard Analysis

  • Andrew IrelandEmail author
  • Maria Teresa Llano
  • Simon Colton
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10811)


Model checking and simulation are powerful techniques for developing and verifying the design of reactive systems. Here we propose the use of a complementary technique – automated theory formation. In particular, we report on an experiment in which we used a general purpose automated theory formation tool, HR, to explore properties of a model written in Promela. Our use of HR is constrained by meta-knowledge about the model that is relevant to hazard analysis. Moreover, we argue that such meta-knowledge will enable us to explore how safety properties could be violated.


Formal methods Verification Hazard analysis 


  1. 1.
    Abrial, J.-R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press, Cambridge (2010)CrossRefzbMATHGoogle Scholar
  2. 2.
    Colton, S.: Automated Theory Formation in Pure Mathematics. Springer, Heidelberg (2002). CrossRefzbMATHGoogle Scholar
  3. 3.
    Colton, S., Bundy, A., Walsh, T.: Automatic invention of integer sequences. In: Proceedings of AAAI (2000)Google Scholar
  4. 4.
    Colton, S., Muggleton, S.: Mathematical applications of inductive logic programming. Mach. Learn. 64, 25–64 (2006)CrossRefzbMATHGoogle Scholar
  5. 5.
    Colton, S., Ramezani, R., Llano, T.: The HR3 discovery system: design decisions and implementation details. In: Proceedings of the AISB Symposium on Computational Scientific Discovery (2014)Google Scholar
  6. 6.
    Holzmann, G.J.: The SPIN Model Checker. Pearson Education, London (2003)Google Scholar
  7. 7.
    Jackson, M.: Problem Frames: Analysing and Structuring Software Development Problems. Addison-Wesley, Boston (2001)Google Scholar
  8. 8.
    Leveson, N.G.: Engineering a Safer World. MIT, Cambridge (2011)Google Scholar
  9. 9.
    Llano, M.T., Ireland, A., Pease, A.: Discovery of invariants through automated theory formation. Formal Aspects Comput. 26, 203–249 (2011)CrossRefGoogle Scholar
  10. 10.
    Reason, J.: Organizational Accidents Revisited. Ashgate, Farnham (2016)Google Scholar
  11. 11.
    Sorge, V., Meier, A., McCasland, R., Colton, S.: Automatic construction and verification of isotopy invariants. J. Autom. Reason. 40(2–3), 221–243 (2008)MathSciNetCrossRefzbMATHGoogle Scholar

Copyright information

© Springer International Publishing AG, part of Springer Nature 2018

Authors and Affiliations

  • Andrew Ireland
    • 1
    Email author
  • Maria Teresa Llano
    • 2
  • Simon Colton
    • 2
    • 3
  1. 1.School of Mathematical and Computer SciencesHeriot-Watt UniversityEdinburghUK
  2. 2.Department of ComputingGoldsmiths, University LondonLondonUK
  3. 3.Games AcademyFalmouth UniversityFalmouthUK

Personalised recommendations