Synthesizing Monitors for Safety Properties - This Time With Calls and Returns -

Rosu, Grigore; Chen, Feng; Ball, Thomas

Permalink

https://hdl.handle.net/2142/11402 Copy

Description

Title

Synthesizing Monitors for Safety Properties - This Time With Calls and Returns -

Author(s)

• Rosu, Grigore
• Chen, Feng
• Ball, Thomas

Issue Date

2007-10

Keyword(s)

computer science

Abstract

We present an extension of past time LTL with call/return atoms, called ptCaRet, together with a monitor synthesis algorithm for it. ptCaRet includes abstract variants of past temporal operators, which can express properties over traces in which terminated function or procedure executions are abstracted away into a call and a corresponding return. This way, ptCaRet can express safety properties about procedural programs which cannot be expressed using conventional linear temporal logics. The generated monitors contain both a local state and a stack. The local state is encoded on as many bits as concrete temporal operators the original formula has. The stack pushes/pops bit vectors of size the number of abstract temporal operators the original formula has: push on begins, pop on ends of procedure executions. An optimized implementation is also discussed and is available to download.

Type of Resource

text

Permalink

http://hdl.handle.net/2142/11402

Copyright and License Information

You are granted permission for the non-commercial reproduction, distribution, display, and performance of this technical report in any format, BUT this permission is only for a period of 45 (forty-five) days from the most recent time that you verified that this technical report is still available from the University of Illinois at Urbana-Champaign Computer Science Department under terms that include this permission. All other rights are reserved by the author(s).

Owning Collections