证明富互联网应用的性质

我们引入了应用层规范，使我们能够推理富互联网应用的状态和事务。我们定义了基于状态/事件的逻辑 UCTL* 的变体，并结合两个示例应用来演示该方法，随后考察了一个分布式富互联网应用，证明了关于其存储和传播信息的性质。我们的方法使我们能够通过互联网环境下具体性质的证明，来论证在并发网络输入面前得以保持的抽象性质的证明。我们得出结论，该方法使得能够可靠且通用地推理构成互联网应用层的程序和协议。