invariants come from templates
We present a template mechanism which allows collective behavior and its invariants to be expressed in an abstract form. The mechanism supplements a view-based decomposition of distributed collaboration. Together templates and composition allow common idioms of distributed behavior to be specified and verified in an abstract form, and to be integrated in specifications. Two templates from a formal specification of Lamport's Paxos algorithm are given as examples.
invariants templates distributed systems closed world views collective behaviour