Abstract
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.
The work reported here is funded by EPSRC Platform Grant EP/N014758/1. We thank the three anonymous NFM 2018 reviewers for their constructive feedback.
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.
HR is derived from the initials of the mathematicians Godfrey Harold Hardy and Srinivasa Aiyangar Ramanujan.
References
Abrial, J.-R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press, Cambridge (2010)
Colton, S.: Automated Theory Formation in Pure Mathematics. Springer, Heidelberg (2002). https://doi.org/10.1007/978-1-4471-0147-5
Colton, S., Bundy, A., Walsh, T.: Automatic invention of integer sequences. In: Proceedings of AAAI (2000)
Colton, S., Muggleton, S.: Mathematical applications of inductive logic programming. Mach. Learn. 64, 25–64 (2006)
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)
Holzmann, G.J.: The SPIN Model Checker. Pearson Education, London (2003)
Jackson, M.: Problem Frames: Analysing and Structuring Software Development Problems. Addison-Wesley, Boston (2001)
Leveson, N.G.: Engineering a Safer World. MIT, Cambridge (2011)
Llano, M.T., Ireland, A., Pease, A.: Discovery of invariants through automated theory formation. Formal Aspects Comput. 26, 203–249 (2011)
Reason, J.: Organizational Accidents Revisited. Ashgate, Farnham (2016)
Sorge, V., Meier, A., McCasland, R., Colton, S.: Automatic construction and verification of isotopy invariants. J. Autom. Reason. 40(2–3), 221–243 (2008)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer International Publishing AG, part of Springer Nature
About this paper
Cite this paper
Ireland, A., Llano, M.T., Colton, S. (2018). The Use of Automated Theory Formation in Support of Hazard Analysis. In: Dutle, A., Muñoz, C., Narkawicz, A. (eds) NASA Formal Methods. NFM 2018. Lecture Notes in Computer Science(), vol 10811. Springer, Cham. https://doi.org/10.1007/978-3-319-77935-5_17
Download citation
DOI: https://doi.org/10.1007/978-3-319-77935-5_17
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-77934-8
Online ISBN: 978-3-319-77935-5
eBook Packages: Computer ScienceComputer Science (R0)