云计算环境下基于不变式的并发分布式算法形式化验证方法研究

With the advent of the era of cloud computing, concurrent and distributed systems are widely used in the Internet, for example, point-to-point application, distributed database, network file system and wireless sensor networks. Validation of concurrent and distributed algorithms has become one of most challenging key issues in current cloud computing environment. Formal verification method not only can consolidate the trust relationship between the cloud service providers and customers, but also find subtle errors hidden in the complicated concurrent and distributed system, which other methods (such as test) are difficult to deal with. Based on our long time’s work in formal specification language and method, algorithm derivation and verification, supported by customize generic abstract design language Apla, further research and put forward a simple, highly abstract language mechanism of concurrent distributed computing, which supports both sequential algorithm verification, and concurrent distributed algorithm verification; Based on the loop invariant new definition and new development strategy which our team proposes, exploring deeply systematic construction method of inductive invariant, and verification method of concurrent distributed algorithms based on inductive invariant; Then study semi-automatically aid verification using theorem prover. Finally, the validation method is applied to verification concurrent distributed algorithms and Web service proxies in the cloud computing environment.

随着云计算时代的到来，并发分布式系统广泛应用于互联网，例如点到点的应用、分布式数据库、网络文件系统和无线传感器网络。并发分布式算法的验证已经成为当前云计算环境下最具挑战性的关键问题之一, 形式化验证方法既能巩固云服务提供者和客户之间的信任关系，又能发现其它方法（如测试）难以发现的隐藏在复杂并发分布式系统中微妙的错误。本项目基于我们在形式化规约语言和方法、算法形式推导和验证方面的长期工作，以自定义泛型抽象顺序设计语言Apla为基础，进一步研究并提出简明、高抽象度并发分布式计算的语言机制，使其既支持顺序算法的验证，又能有效的验证并发分布式算法；基于我们团队提出的循环不变式的新定义和新的开发策略，深入探索归纳不变式的系统构造方法，及基于归纳不变式的并发分布式算法的验证方法；进而研究使用定理证明器半自动化进行辅助验证。最后，将该验证方法应用到云计算环境下并发分布式算法和Web服务协议的验证。

随着云计算时代的到来，并发分布式系统广泛应用于互联网，例如点到点的应用、分布式数据库、网络文件系统和无线传感器网络。并发分布式算法的验证已经成为当前云计算环境下最具挑战性的关键问题之一, 形式化验证方法既能巩固云服务提供者和客户之间的信任关系，又能发现其它方法（如测试）难以发现的隐藏在复杂并发分布式系统中微妙的错误。本项目基于我们在形式化规约语言和方法、算法形式推导和验证方面的长期工作，以自定义泛型抽象顺序设计语言Apla为基础，进一步研究并提出简明、高抽象度并发分布式计算的语言机制，使其既支持顺序算法的验证，又能有效的验证并发分布式算法；基于我们团队提出的循环不变式的新定义和新的开发策略，深入探索归纳不变式的系统构造方法，及基于归纳不变式的并发分布式算法的验证方法；进而研究使用定理证明器半自动化进行辅助验证。项目取得了一系列研究成果。发表期刊论文21篇，会议论文6篇。出版学术专著3部。授权专利1个，软件著作权6个。培养青年教师和研究生共计13名，获国家级创新创业奖励9次。项目研究成果对云计算环境下并发分布式算法和Web服务协议的验证具有重要的理论意义和应用价值。