From model checking to a temporal proof for partial models: preliminary example
arXiv:1706.02701
Abstract
This paper describes in detail the example introduced in the preliminary evaluation of THRIVE. Specifically, it evaluates THRIVE over an abstraction of the ground model proposed for a critical component belonging to a medical device used by optometrists and ophtalmologits to dected visual problems.
5 pages, 3 figures