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.