JPL Technical Report Server

Runtime Verification Logics A Language Design Perspective

Show simple item record

dc.contributor.author Havelund, Klaus
dc.contributor.author Reger, Giles
dc.date.accessioned 2020-03-11T21:29:54Z
dc.date.available 2020-03-11T21:29:54Z
dc.date.issued 2017-08-21
dc.identifier.citation MFCS 2017: 42nd International Symposium on Mathematical Foundations of Computer Science, Aalborg, Denmark, August 21-25, 2017 en_US
dc.identifier.clearanceno CL#17-2207
dc.identifier.uri http://hdl.handle.net/2014/47521
dc.description.abstract Runtime Verification is a light-weight approach to systems verification, where actual executions of a system are processed and analyzed using rigorous techniques. In this paper we shall narrow the term’s definition to represent the commonly studied variant consisting of verifying that a single system execution conforms to a specification written in a formal specification language. Runtime verification (in this sense) can be used for writing test oracles during testing when the system is too complex for full formal verification, or it can be used during deployment of the system as part of a fault protection strategy, where corrective actions may be taken in case the specification is violated. Specification languages for runtime verification appear to differ from for example temporal logics applied in model checking, in part due to the focus on monitoring of events that carry data, and specifically due to the desire to relate data values existing at different time points, resulting in new challenges in both the complexity of the monitoring approach and the expressiveness of languages. Over the recent years, numerous runtime verification specification languages have emerged, each with its different features and levels of expressiveness and usability. This paper presents an overview and a discussion of this design space. en_US
dc.description.sponsorship NASA/JPL en_US
dc.language.iso en_US en_US
dc.publisher Pasadena, CA: Jet Propulsion Laboratory, National Aeronautics and Space Administration, 2017 en_US
dc.title Runtime Verification Logics A Language Design Perspective en_US
dc.type Preprint en_US


Files in this item

This item appears in the following Collection(s)

Show simple item record

Search


Browse

My Account