The use of automated theory formation in support of hazard analysis

Research output: Chapter in Book/Report/Conference proceedingConference PaperResearchpeer-review


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.

Original languageEnglish
Title of host publicationNASA Formal Methods
Subtitle of host publication10th International Symposium, NFM 2018 Newport News, VA, USA, April 17–19, 2018 Proceedings
EditorsAaron Dutle, Cesar Munoz, Anthony Narkawicz
Place of PublicationCham Switzerland
Number of pages7
ISBN (Electronic)9783319779355
ISBN (Print)9783319779348
Publication statusPublished - 2018
Externally publishedYes
Event10th International Symposium on NASA Formal Methods, NFM 2018 - Newport News, United States of America
Duration: 17 Apr 201819 Apr 2018

Publication series

NameLecture Notes in Computer Science
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Conference10th International Symposium on NASA Formal Methods, NFM 2018
CountryUnited States of America
CityNewport News


  • Formal methods
  • Hazard analysis
  • Verification

Cite this