概率系统的模型检验与其应用

Formal verification techniques have been successfully applied to complex systems such as the IEEE Futurebus+ standard, Needham-Schroeder authentication algorithm and ISDN protocols. Recently, quantitative verification has become an important extension of the basic approach towards verifying systems involving probabilities, costs, and continuous-time. These characteristics are the key ingredients for modeling and analyzing networked, embedded, biological and energy systems. On the other side, the systems we are facing today are becoming more and more complex, and consist of many components. Indeed, the challenge of verifying such systems is the famous state-space explosion problem: the verification effort needed generally increases exponentially with their components. The goal of this project is to identify efficient verification techniques that are the most promising for analyzing large scale probabilistic systems. We shall focus especially on bisimulation minimization, compositional verification, and on-the-fly verification techniques for probabilistic systems. On the practical side, we plan to enrich our probabilistic model checker IscasMC to support richer models, efficient algorithms, friendly user interfaces. Our vision is to bring IscasMC an internationally recognized tool in the probabilistic verification community, which can compete with the leading tool PRISM in some respect.

形式化验证技术已被成功的应用到诸如ISDN协议、IEEE Futurebus标准和Needham-Schroeder认证协议等的验证中。近来，国内外学者将研究焦点逐渐转移到包含概率、报酬（reward）、时间等的概率模型及其扩展中来。这些是刻画网络协议、嵌入式系统、生物及能源系统的关键元素。 另一方面，现今系统建模的复杂度急剧增加、其包含的组件数目越来越多。我们面临着著名的状态空间爆炸问题：模型的状态空间往往成指数爆炸趋势增长。本项目的目标是研究高效的概率模型检验技术。我们将研究互模拟状态优化、组合验证和概率模型的on-the-fly验证技术。从实践的角度来说，我们将扩展我们的概率模型检验工具IscasMC，使其支持更多模型种类、高效算法及友好的图形界面。我们的目标是把IscasMC发展成在国际同行有影响力的工具,使它能够分析复杂的系统，并在某些方面能超过PRISM等国际知名工具。

形式化验证技术已被成功的应用到诸如ISDN协议、IEEE Futurebus标准和Needham-Schroeder认证协议等的验证中。近年来，国内外学者将研究焦点逐渐转移到包含概率、报酬（reward）、时间等的概率模型及其扩展中来。这些是刻画网络协议、嵌入式系统、生物及能源系统的关键元素。另一方面，现今系统建模的复杂度急剧增加、其包含的组件数目越来越多。我们面临着著名的状态空间爆炸问题：模型的状态空间往往成指数爆炸趋势增长。本项目的目标是研究高效的概率模型检验技术。我们对互模拟状态优化、组合验证和概率模型的on-the-fly验证技术进行了深入的研究。从实践的角度来说，我们扩展了我们的概率模型检验工具IscasMC，使其能够支持更多模型种类、高效算法及友好的图形界面。