大规模概率并发实时系统模型检验

This project deals with model checking problem of large scale models exhibiting both probabilistic and timed behaviors. Probabilities and times are two key components in modelling and analyzing real-time systems, security systems, and network systems. Because of the state-space explosion problem for concurrent systems, the model checking problem remains as a big challenge in the community. The goal of this project is to tackle main research challenges, including (i) appropriate high-level modelling language for modelling concurrency, probability and time, (ii) characterization and decomposition of temporal properties, (iii) symbolic data structure, and efficient model checking algorithm for both qualitative and quantitative properties. Our key techniques are a divide-and-conquer approach to the property analysis, applying linear-programming techniques in solving the core quantitative measures, and applying learning algorithms to get small abstraction. We will build a tool, implement our algorithms and analyse case studies of large scale.

本项目致力于大规模概率并发实时系统的模型检验问题。在对实时系统、安全系统和网络系统的建模与分析中，概率和时间是这些系统的关键组成部分。由于在并发系统中验证中出现的状态爆炸问题，模型检验问题在学术界依然是巨大的挑战。本项目的目标是解决下面重要的科研挑战：一、描述并发、概率和时间三要素的高层建模语言；二、时序性质的刻画与分解；三、性质定性和定量分析所需要的符号化数据结构与高效模型检验算法。我们的关键技术是首先采取分而治之的方法进行性质分析，然后利用线性规划技术来解决核心的定量分析问题，同时应用学习算法来获取系统更小的抽象表示。我们将上述算法和理论实现在一个工具中，并用其来分析大规模概率并发实时系统实例。

本项目开展了针对大规模概率并发实时系统的模型检验问题的研究。我们提出了基于Reo语言的建模框架及基于时序逻辑的验证框架，并为解决复杂系统模型检验中的状态空间爆炸问题提出了一系列理论与方法。主要贡献为：. 我们提出了一个组合建模框架，能够同时支持系统的时间、概率和并发元素。我们对Reo建模语言进行了概率及实时扩展，称之为Mediator。同时，我们进一步对其组件与中间件语义进行扩展，用以有效地自动构建模型，以及设计基于组件的验证框架。. 针对复杂性质规约，我们研究了如何将其分割成不同类别的子性质，如安全性、活性和公平性，并研究其对应高效可达性、终止性判定问题。我们进而研究了高效的符号数据结构，以实现相应模型的高效存储与验证算法。针对大规模系统的验证，我们进一步利用基于模拟与互模拟最小化的抽象和分析技术，从而约减验证中的状态空间以突破传统验证方法的效率瓶颈。. 模型验证的反例分析是验证反馈循环中的关键环节。我们重点研究了反例指导的抽象优化技术。我们对原系统的抽象模型上不成立的性质验证生成一个反例，若该反例不是原系统的反例，则说明学习得到的抽象模型不能精确地反映原系统的性质。此时，我们针对假反例对学习模型进行优化。进一步，我们将模型学习框架扩展到黑盒系统的分析中，如应用L*学习算法来对模型进行建模验证。. 基于本项目所研发的方法与技术，项目组开发了一整套大规模概率并发实时系统模型检验的平台ePMC，并将其应用于现实中如通信协议、汽车控制系统等大规模概率并发实时系统的建模和分析中。成果方面，我们发表了90余篇论文，其中包括24篇CCF A级论文。我们的验证平台获得了国际学术与产业界的关注，并被华为公司应用于大型分布式数据库协议的分析中。最后，通过这个项目，我们和德国课题组之间建立了稳定的合作关系，并与萨尔大学、MPI等联合组建了中欧可靠智能软件联合实验室。