实时环境下概率程序的符号验证方法及其参数化扩展

Nowadays, information technologies have a deep impact on all aspects of our daily life. How to improve the reliability of software systems is an inevitable problem. To pursue the absolute correctness, formal verification methods, which are based on all kinds of symbolic reasoning techniques, came into being. Most traditional verification methods are designed solely for deterministic programs, but not well suitable for probabilistic ones. However, along with the rapid development of machine learning, information security and quantum computing, probabilistic programs acting as a powerful describing language in those fields become more and more popular. So it is entirely worth studying the specialized verification methods for probabilistic programs. This project investigates some probabilistic programs in real-time environment. We aim to present exact algorithms to effectively compute the termination probabilities and the expectations of expressions, and thereby rigorously reason about program properties. The aforementioned algorithms would be extended to parametric program models. From the specification, we are to directly infer the feasible regions and the optimal solutions of the parameters, and thereby complete the formal software design in a forward way. All these results would be served as a solid theoretical basis of modern trustworthy software. Besides, our preliminary results reveal that the advance on verifying probabilistic programs would also drive that on symbolic computation, and the two issues would be mutually motivated and developed. Finally this project plans to provide efficient verification tools for academic communications.

现今信息技术已经渗透到日常生活的方方面面。如何提高软件系统的可靠性是一个不可回避的问题。为了追求绝对正确性这目标，基于各种符号推理技术的形式化验证方法应运而生。传统的验证方法往往针对确定性程序而设计，并不完全适用于概率程序。特别是，随着近年来机器学习、信息安全、量子计算等领域的迅猛发展，概率程序作为这些领域最通用描述语言之一，相应的验证方法就格外值得我们去研究。本项目就以若干实时环境下的概率程序为研究主体，拟提出能有效计算终止概率、表达式期望的一些准确算法，从而严格推理软件程序性质；并在参数化的程序模型上做扩展，从规范出发，直接推导参数的可行域、最优解，完成正向的形式化软件设计。这些工作都将为现代可信软件提供扎实的理论基础。此外，预研结果表明，概率程序验证方法的研究也将带动符号计算技术的发展，两者起到相辅相成的效果。最后，本项目还计划研制相应的高效验证工具包，供国内外同行交流。

现今信息技术已经渗透到日常生活的方方面面。如何提高软件系统的可靠性是一个不可回避的问题，特别是应对现今广泛使用的概率系统。本项目主要以实时环境下的概率程序为研究对象，提出能准确计算终止概率、表达式期望的算法，从而严格推理软件程序性质；并在参数化的程序模型上做扩展，从规范出发，直接推导参数的可行域、最优解，完成正向的形式化软件设计。具体成果体现在：i)时滞概率程序的终止性分析，ii)期望表达式的敏感性分析，和iii)概率程序的模型参数合成。现有研究结果也充分证实了概率程序验证和符号计算方法能够相互渗透，互为促进发展。此外，在项目开展过程中，我们认识到量子模型是概率模型的重要延伸。因而，本项目所提出的验证方法体系将在该新兴领域上有着广阔的发展前景。.在本项目支持下，我们已发表10余篇学术论文，包括Inf. Comput.、J. Autom. Reason.、Theoret. Comput. Sci.权威期刊论文4篇和CONCUR会议论文等，均为第一标注；我们培养研究生9名，其中1名博士生和4名硕士生已毕业，圆满完成原定研究目标。根据学界的最新热点，建议后续工作可由概率型计算模型转向量子型计算模型，以期取得丰硕成果。