On safety properties and their monitoring

15Citations
Citations of this article
10Readers
Mendeley users who have this article in their library.

Abstract

This paper addresses the problem of runtime verification from a foundational perspective, answering questions like "Is there a consensus among the various definitions of a safety property?" (Answer: Yes), "How many safety properties exist?' (Answer: As many as real numbers), 'How difficult is the problem of monitoring a safety property?" (Answer: Arbitrarily complex), "Is there any formalism that can express all safety properties?" (Answer: No), etc. Various definitions of safety properties as sets of execution traces have been proposed in the literature, some over finite traces, others over infnite traces, yet others over both finite and infinite traces. By employing cardinality arguments and a novel notion of persistence, this paper rst establishes the existence of bijective correspondences between the various notions of safety property. It then shows that safety properties can be characterized as "always pas" properties. Finally, it proposes a general notion of monitor, which allows to show that safety properties correspond precisely to the monitorable properties, and then to establish that monitoring a safety property is arbitrarily hard. © Scientific Annals of Computer Science 2012.

Cite

CITATION STYLE

APA

Roşu, G. (2012). On safety properties and their monitoring. Scientific Annals of Computer Science, 22(2), 327–365. https://doi.org/10.7561/SACS.2012.2.327

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free