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

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

项目编号： No.61262002

项目类型： 地区科学基金项目

立项/批准年度： 2013

项目学科： 自动化技术、计算机技术

项目作者： 肖芳雄

作者单位： 广西财经学院

项目金额： 43万元

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

英文关键词： Process Algebra；Model Checking；Time；Space；