建立适用于自适应软件系统的在线概率模型检测技术

With the rise of large-scale systems such as cyber-physical systems and online business-critical systems, the development of high-quality control software components for those systems becomes an increasingly important challenge. Traditional software engineering usually does not include well understood and applied methods for control modeling. Theoretical methods in the control system research (e.g., control theory, machine learning and Bayesian decision theory), on the other hand, does not support the design of software in the software architectural level. The proposed project aims to establish a comprehensive and practical model-reasoning technology for self-adaptive software systems, namely software systems whose architecture is evolutional after their deployment. Main research objectives will include a systematic theoretical framework based on online probabilistic model checking, a tool and case studies to experiment with our novel methods and algorithms. Key questions of the proposed project will be the following three: How to incorporate complex methods of statistical inference into parametric probabilistic model checking; how to use iterative methods to balance between the sample size of system parameters and the correctness rates of verification results; how to achieve a parametric probabilistic model checking method for continuous-time models. If successful, the proposed project will improve the state-of-the-art in the intersection of software engineering and control systems.

随着信息物理系统和在线的业务关键型系统等大型系统的兴起，如何为这些系统的软件开发高质量的控制组件成为迫切需要解决的问题。传统的软件工程领域不包含控制建模的方法，而控制系统领域现有理论方法——如控制论、机器学习以及贝叶斯决策论——尚未能在软件体系结构层面为软件开发提供支持。本项目旨在为自适应软件系统这一类具有进化型体系结构的软件系统建立一项完备和适用的模型推理技术。研究内容包括：(1) 建立一个基于在线概率模型检测的、系统性的理论框架；(2) 开发一个工具来实现理论框架的新方法和算法，并利用该工具进行案例分析。而研究的关键问题是：(1) 如何把复杂的统计推断方法结合到参数化概率模型检测中；(2) 如何利用迭代的方法来平衡系统参数的采样大小和结果的正确率；(3) 如何建立连续时间的模型检测的参数化方法。本项目的意义在于提高软件工程和控制系统的交叉领域的科研水平。

随着服务计算和信息物理系统的迅速发展，对软件系统的自适应性的要求越来越高。概率模型检测是一项强大的形式化验证技术，能否严格地分析广泛存在于不同领域的随机系统，但是应用于自适应软件系统的分析上，这项技术仍然存在理论上的困难点。本项目的目标是建立一个适用于自适应软件系统分析的在线概率模型检测的技术框架，重要解决如何为经验参数建模，如何平衡时时效性和精确性，以及如何提高概率模型检测的预算效率这三个关键问题。..在所取得一系列项目研究成果中，我们把最重要的成果总结成以下两点：第一、我们利用敏感度分析方法来处理对带经验参数的随机系统模型的验证。传统的概率模型检测要求所有参数值必须精确地给出，但是软件系统的某些参数由系统运行数据决定，这种不精确性会对验证输出产生影响，在某些情况下还会造成对验证结果的误判。我们提出新的数值计算方法，来计算验证输出相对于模型不精确性的敏感度（即一阶和高阶偏导），在利用近似优化方法来得到影响的最值。跟相处的参数化概率模型检测和区间值概率模型检测等最新方法相比，我们的方法在计算上更有效率，可应用的范围（即适用的模型种类）也更广。第二、我们将统计推断引入概率模型检测中，来分析模型参数的采样大小与验证输出的置信度之间的关系。作为形式化验证技术，传统的概率模型检测无法对验证结果的统计意义作出判断，我们将概率模型检测看出从模型参数的随机变量到验证输出的变量的一个变换，利用上述敏感度计算方法求得偏导，从而进行多元统计推断。..总而言之，我们的项目成果不仅改进了概率模型检测的理论，将它从一项传统的线下验证技术提升为现代的在线分析方法，还拓展了它的应用范围，使它适用于安全关键型和需求关键型的软件系统的监控。