论文标题
建立服务水平协议的对称协议
A symmetric protocol to establish service level agreements
论文作者
论文摘要
我们提出了一种对称协议，以反复协商两个方之间的所需服务水平，在该方面，服务级别是从一些完全有序的有限域中获取的。同意的服务级别是从双方和各方动态提出的级别中选择的，只能在谈判期间降低所需的服务水平。使用模态公式说明了协议的正确性，并使用外部行为模量模量弱痕量等效性和呈差异分支分支分支的行为降低来解释其行为。我们的协议源自工业用例，事实证明正确设计非常棘手。
We present a symmetrical protocol to repeatedly negotiate a desired service level between two parties, where the service levels are taken from some totally ordered finite domain. The agreed service level is selected from levels dynamically proposed by both parties and parties can only decrease the desired service level during a negotiation. The correctness of the protocol is stated using modal formulas and its behaviour is explained using behavioural reductions of the external behaviour modulo weak trace equivalence and divergence-preserving branching bisimulation. Our protocol originates from an industrial use case and it turned out to be remarkably tricky to design correctly.
