Hierarchical Protocol Analysis by Temporal Logic

With an example,this paper describes a method of using temporal logic for stepwise analysis of protocol specifications.Each level in the specified hierarchy is a kind of incarnation from higher-levels by adding some implementation strategies,and the correctness of top-down refinements could be verified in the unified temporal framework.