Hierarchical Protocol Analysis by Temporal Logic

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