噪音环境下移动进程的可靠性与安全性

为了形式化建模和分析移动系统，图灵奖得主Milner等人创建了移动进程理论pi-演算。pi-演算是一类进程代数，进程之间的(无噪音)通信是其最重要的组成部分。考虑到实际系统中信道噪音难以避免，应明生教授最近建立了一种带噪音的pi-演算。本项目旨在结合香农信息论和进程代数理论，在恰当建模的基础上，研究噪音环境下移动进程的可靠性和安全性。我们将发展一个新的，忠实的带噪音pi-演算，讨论它的基本性质，揭示该演算与概率pi-演算的联系。在此基础上，结合互模拟概念，定义可靠性度量并研究如何提高噪音环境下移动进程的可靠性。进一步，我们将研究基于pi-演算及其扩展spi-演算的密码协议在噪音环境下的安全性。同时，我们也将结果应用于分析进程代数建模的服务计算中服务的可靠性与安全性。本项目的研究将有助于设计移动系统（如Internet，移动通信系统），分析和严格推理它们行为的可靠性和安全性。

为了形式化建模和分析移动系统，图灵奖得主Milner等人创建了移动进程理论pi-演算。pi-演算是一类进程代数，进程之间的（无噪音）通信是其最重要的组成部分。考虑到实际系统中信道噪音难以避免，应明生教授建立了一种带噪音的pi-演算。本项目结合香农信息论和进程代数理论，在恰当建模的基础上，比较系统和深入地研究了噪音环境下移动进程的可靠性。我们发展了一个新的、忠实的带噪音pi-演算，讨论了它的基本性质，揭示了该演算与概率pi-演算间的联系。在此基础上，结合互模拟概念，定义了可靠性度量，并研究了如何提高噪音环境下移动进程的可靠性。同时，我们研究了条件匿名性，可用于分析密码协议在噪音环境下的安全性。另外，我们也将相关思想和结果应用于业务处理执行语言BPEL和BPEL4People、实时和嵌入式系统规范序列图等的建模与分析。本项目的研究成果为设计可靠、安全的移动系统（如Internet，移动通信系统）奠定了基础。