@article{gerard_singh_2013, title={Formalizing and Verifying Protocol Refinements}, volume={4}, ISSN={["2157-6912"]}, url={http://www.scopus.com/inward/record.url?eid=2-s2.0-84876124077&partnerID=MN8TOARS}, DOI={10.1145/2438653.2438656}, abstractNote={
            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 the
            refinement
            of one protocol by another. Refinement for protocols is both intuitively obvious (e.g.,
            PayViaCheck
            is clearly a kind of
            Pay
            ) and technically nontrivial (e.g., compared to
            Pay
            ,
            PayViaCheck
            involves 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.
          }, number={2}, journal={ACM TRANSACTIONS ON INTELLIGENT SYSTEMS AND TECHNOLOGY}, author={Gerard, Scott N. and Singh, Munindar P.}, year={2013}, month={Mar} }