Formalizing and verifying protocol refinements
Scott N. Gerard, Munindar P. Singh · ACM Transactions on Intelligent Systems and Technology · 2013
A (business) protocol describes, in high-level terms, a pattern of communication between two or more participants, specifically via the creation and manipulation of the commitments between them. In this manner, a protocol offers both flexibility and rigor: a participant may communicate in any way it chooses as long as it discharges all of its activated commitments. Protocols thus promise benefits in engineering cross-organizational business processes. However, software engineering using protocols presupposes a formalization of protocols and a notion of therefinementof one protocol by another. Refinement for protocols is both intuitively obvious (e.g.,PayViaCheckis clearly a kind ofPay) and technically nontrivial (e.g., compared toPay,PayViaCheckinvolves different participants exchanging different messages). This article formalizes protocols and their refinement. It develops Proton, an analysis tool for protocol specifications that overlays a model checker to compute whether one protocol refines another with respect to a stated mapping. Proton and its underlying theory are evaluated by formalizing several protocols from the literature and verifying all and only the expected refinements.