Internet环境下组合式软件的时空进程代数刻画及模型检测

Formal methods have been exploited to model and verify software on aspects of functionality,time and space, so that we can get insight and confidence about softwares. Process algebras are a kind of formal models that are suitable to model and verify concurrent and composite systems,including Internet Composite Softwares(ICS),e.g., internetware and Web services composition. Currently, process algebras are maily used to model and verify functional aspects,not including non-functional aspcts, which is not enough for us to get insight and confidence for ICS. Hence, on one hand, we will propose Time-Space Progess Algebra(TSPA) based on Interactive Markov Process Algebra, and we want that TSPA has capability to model functinal aspects, time performace and space performance in unification from ICS's behavior view, so that we can get insight and confidence about ICS. On the other hand, we will propose Time-Space Logic(TSL) based on Action Continue Stochastic Logic, and we want that TSL has capability to model functional aspects,time performance and space performance in unification form ICS's property view. Further, we will research on model checking algorithm that should support both TSPA and TSL, and will apply the algorithm for an ICS.

为软件提供合适的形式化理论模型，并在模型上刻画和验证软件的功能特性、时间特性和空间特性，是充分反映软件的本质和特征，提高软件可信性的重要途径。进程代数是一种适合刻画和验证并发组合系统的形式化系统，目前进程代数对Internet环境下的组合式软件（如网构软件、Web服务组合等）的刻画和验证主要集中在功能方面，未能充分反映这类软件的特性。本项目拟在交互式马尔可夫进程代数的基础上研究时空进程代数，支持从行为的角度对组合式软件的功能特性、时间特性、空间特性的统一刻画。此外为支持对组合式软件的这些特性进行统一模型检测，本项目拟在动作连续随机逻辑基础上研究时空逻辑，支持从性质的角度对组合式软件的功能特性、时间特性、空间特性的统一刻画。在此基础上，本项目研究支持时空进程代数和时间逻辑的模型检测算法，并对Internet环境下组合式软件实例的功能特性、时间特性和空间特性统一进行验证。

中文摘要(对项目的背景、主要研究内容、重要结果、关键数据及其科学意义等做简单概述，800字以内)：. . 进程代数是适合组合软件建模和验证的形式化系统，模型检测是目前流行的一种自动化形式验证方法，在传统进程代数基础上研究能够统一刻画功能属性、时间属性和空间属性的进程代数并用于Internet组合式软件的模型检测，对于保障该类软件的质量具有重要意义。我们做了如下研究工作并取得了相应成果。(1)研究了统一刻画功能属性、时间属性和空间属性的时空进程代数，给出了语法和语义,以及状态空间构造算法，给出了时空进程代数互模拟的语法和语义,互模拟判定算法；(2)研究了统一刻画功能属性、时间属性和空间属性的时空逻辑，给出了时空逻辑的语法、语义和公理系统, 给出了时空逻辑的路径公式和状态公式的语法及语义，给出了时空逻辑的路径公式和状态公式的模型检测算法；(3)研究了模型检测中减轻状态空间爆炸问题的方法和途径，包括基于抽取-精化的概率系统假设-保证验证，基于抽象解释的服务间消息模型检测的数据约减，BPEL谓词约束建模与可行路径分析等；(4)把时间、概率、代价等时空属性扩展进UML基本序列图和高层序列图中，使得扩展后的UML序列图可以建模组合式软件的功能行为及时空特性，且因为是图形化建模方式，易于被最终用户、需求分析人员和系统设计人员理解和掌握，有利于产业化推广和使用；(5)扩展时空序列图到时空进程代数的转换实现，使得扩展时空属性后的UML序列图易于被最终用户、需求分析人员和系统设计人员理解和掌握，可以用来建模组合式软件的功能行为及时空特性，具有图形化建模方式带来的方便易用的好处，进一步转化为TSPA形式化模型，具有形式化自动分析验证的好处，有利于产业化推广和使用。