From model checking to a temporal proof for partial models: preliminary example
Logic in Computer Science
2017-06-12 v1
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.
Cite
@article{arxiv.1706.02701,
title = {From model checking to a temporal proof for partial models: preliminary example},
author = {A. Bernasconi and C. Menghi and P. Spoletini and L. D. Zuck and C. Ghezzi},
journal= {arXiv preprint arXiv:1706.02701},
year = {2017}
}
Comments
5 pages, 3 figures