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


الملخص بالإنكليزية

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.

تحميل البحث