多角色协同系统的定量验证方法研究

Due to the characteristics of multi-role collaborative systems and the shortage of PRISM, this project proposes a method on quantitative verification for multi-role collaborative systems based on strategy, which is the integration of the formal method, the probabilistic mathematical theory and model verification technology. First the probabilistic strategy logic language moPSL is proposed, which can formalized describe the strategy used by each role and the relationship among strategies; then the multi-objective verification method based on strategy is proposed. This method combines the value iteration with strategy to choose the path, and a new termination criterion is studied to find the ε-optimal strategy or counterexamples.Finally the quantitative verification tool PLSQM is constructed. Therefore, the research in this project will add the function of describing the strategy to logical language, enhance the reasoning and verification ability of probability automaton model, solve the space explosion problem caused by too much state of the models, and improve verification efficiency and the correctness of the software, so that it can provide support for the analysis and construction of multi-role cooperative systems with high reliability.More than 3 papers indexed by SCI are expected to publish, 1 invention patent is applied.

本课题综合运用形式化方法、概率数学理论和自动机理论，针对多角色协同系统软件的特点及目前定量验证工具PRISM存在的不足，提出了基于策略的定量验证方法。该方法首先提出多目标概率策略逻辑语言moPSL，使其可以形式化描述系统中每个角色所使用的策略及策略之间的相互关系；然后提出基于策略的限界模型多目标定量验证方法，该方法将数值迭代与策略相结合用于选择路径，并且重新定义限界模型检测的终止条件，从而找到ε最优解或者反例；最后构建定量验证工具PLSQM。本研究能够增强逻辑语言对角色所使用的策略的描述能力，增强概率自动机模型的推理与验证能力，解决系统中模型状态过多引起的空间爆炸问题，提高验证效率与软件正确性，为分析和构建高可靠性的多角色协同系统提供支持。预期发表SCI文章3篇以上，申请发明专利1项。

随着计算机技术的发展，多角色协同系统的软件规模越来越大、复杂性日趋增加，如何保证其正确性和可靠性成为日益紧迫的问题。.本课题针对多角色协同系统的特点及目前定量验证方法中的不足，围绕逻辑语言及定量验证方法展开研究。首先我们研究了定量验证中常用的逻辑语言，提出了概率实时逻辑语言PTSL，该逻辑语言显式的把策略作为一阶逻辑中的对象，从而使我们能够以简单而自然的方式指定多角色协同系统中的非零和属性；然后提出了基于消息传递的限界模型定量验证方法的研究。我们前期已经对Prism工具中定量验证算法进行了研究，其采用的基于值迭代的检测算法工作效率低下，本课题提出了基于消息传递的限界模型检测算法，只有当某个状态的值发生变化时，才会发送消息到它的下一个节点，而没有发生变化的节点不会发送任何信息。从而大大减少了节点发送的消息，提高了工作效率。（3）验证工具研究。本课题将大数据平台Giraph引入系统中，并在上面完成了定量验证算法。以ZeroConf为例，经过分析，使用基于Giraph的定量验证算法比基于值迭代的定量验证算法大大节省了迭代次数。.项目资助发表SCI论文2篇，待发表1篇。申请1项发明专利。