Formal Verification of a Parameterized Data Aggregation Protocol

摘要

We report on our experiences on the successful verification of a parameterized wireless fault-tolerant data aggregation protocol. We outline our verification method that involves automatic verification of a model of the node processing algorithm under system topology constraints. The presented work forms the basis for a generalization to verification rules for aggregation protocols that integrate automatic verification into an inductive framework.