FiLM: A Runtime Monitoring Tool for Distributed Systems
It is well recognized that debugging or testing a distributed system is a great challenge. FiLM is a runtime monitoring tool that can monitor the execution of distributed applications against LTl specifications on finite traces. Implemented within the online predicate checking infrastructure D3S, FiLM models the execution of distributed applications as a trace of consistent global snapshots with global timestamps, and it employs finite automata constructed from LTL specifications to evaluate the trace of distributed systems. We proved that the generated automata accept exactly the traces which satisfy LTL specifications. Our case study shows that FiLM successfully detected an important and intricate liveness bug in a real Paxos implementation.
runtime monitoring finite automata LTL distributed systems
Fuyuan Zhang Zhengwei Qi Haibing Guan Xuezheng Liu Mao Yang Zheng Zhang
School of Software Shanghai Jiao Tong University Shanghai, China School of Software Shanghai Jiao Tong University Shanghai,China System Research Group Microsoft Research Asia Beijing, China System Research Group Microsoft Research Asia Beijing,China
国际会议
上海
英文
40-46
2009-07-08（万方平台首次上网日期，不代表论文的发表时间）