Yliès Falcone, Laurent Mounier, Jean-Claude Fernandez, Jean-Luc Richier
Extending the Safety-Progress Classification of Properties in a Runtime Verification Context (2009)
Extending the Safety-Progress Classification of Properties in a Runtime Verification Context (2009)
TR-2009-5.pdf
Keywords: r-property, safety-progress, hierarchy, runtime verification, Streett, DFA, safety, guarantee, response, persistence
Abstract: This paper revisit and extends results about the Safety-Progress classification of properties introduced by Chang, Manna, and Pnueli. Our work is motivated by runtime verification, as so we believe that this general classification is a good basis for specifying properties. In runtime verification, a major and distinguishing feature is the interest of finite execution sequences and their validation of properties. Indeed, finite execution sequences are often abstract representation of incremental chunks of a program execution. These executions sequences are fed to a monitor, ie a mechanism designed to state appraisal wrt. a desired property under scrutiny. We show in this paper, that the four views originally dedicated to infinitary properties can be uniformly extended to finitary ones.
