Trustworthy Global Computing
Trustworthy Global Computing
复制标题
值得信赖的全球计算
DOI：
10.1007/978-3-642-41157-1_7
复制
发表时间：
2013
期刊：
影响因子：
--
通讯作者：
Bocchi L
中科院分区：
文献类型：
--
作者：
Bocchi L
最近的工作增强多方会话类型的逻辑注释，使不仅验证的结构属性的对话和消息的种类，但也验证的实际值交换的属性。然而，规范和多个跨会话交互的相互影响的验证仍然是一个悬而未决的问题。我们引入了一个多方逻辑证明系统与虚拟状态，使易处理的规范和验证细粒度的会话间的正确性属性的进程参与几个交错的会话。本文提出了一种比较完善的静态验证方法。
Recent work on the enhancement of multiparty sessions types with logical annotations enables not only the validation of structural properties of the conversations and on the sorts of the messages, but also the validation of properties on the actual values exchanged. However, the specification and verification of the mutual effects of multiple cross-session interactions is still an open problem. We introduce a multiparty logical proof system with virtual states that enables the tractable specification and validation of fine-grained inter-session correctness properties of processes participating in several interleaved sessions. We present a sound and relatively complete static verification method.