Abstract
In this paper we describe the formal specification and verification of the efficient algorithm for real-time model checking implemented in the model checker RAVEN. It was specified and proved using the KIV system. We demonstrate how to decompose the correctness proof into several independent subtasks and indicate the corresponding verification efforts. The formal verification revealed some errors, reduced the code size, and improved the efficiency of the implementation.
Cite
CITATION STYLE
Reif, W., Ruf, J., Schellhorn, G., & Vollmer, T. (2000). Do you trust your model checker? In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1954, pp. 179–196). Springer Verlag. https://doi.org/10.1007/3-540-40922-x_12
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
