From model checking to a temporal proof for partial models: preliminary example

A. Bernasconi, C. Menghi, P. Spoletini, L. D. Zuck, C. Ghezzi

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.

Knowledge Graph



Sign up or login to leave a comment