Lecture Notes in Computer Science, 2008, Volume 5289/2008, 51-68, DOI: 10.1007/978-3-540-89247-2_4

Synthesizing Monitors for Safety Properties: This Time with Calls and Returns

Grigore Roşu, Feng Chen and Thomas Ball

View Related Documents

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.
Supported by NSF CCF-0448501, NSF CNS-0509321, NASA ARMD safety Program and Air Force STTR phase I award (Topic Number AF07-T019, Proposal Number F074-019-0162).

Fulltext Preview

Image of the first page of the fulltext document