TY - GEN
T1 - Synthesizing monitors for safety properties
T2 - 8th International Workshop on Runtime Verification, RV 2008
AU - Roşu, Grigore
AU - Chen, Feng
AU - Ball, Thomas
N1 - Funding Information:
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).
PY - 2008
Y1 - 2008
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=57049173078&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=57049173078&partnerID=8YFLogxK
U2 - 10.1007/978-3-540-89247-2_4
DO - 10.1007/978-3-540-89247-2_4
M3 - Conference contribution
AN - SCOPUS:57049173078
SN - 354089246X
SN - 9783540892465
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 51
EP - 68
BT - Runtime Verification - 8th International Workshop, RV 2008, Selected Papers
PB - Springer
Y2 - 30 March 2008 through 30 March 2008
ER -