基于Petri网的构件组装正确性研究

项目名称： 基于Petri网的构件组装正确性研究

项目编号： No.60873061

项目类型： 面上项目

立项/批准年度： 2009

项目学科： 武器工业

项目作者： 王捍贫

作者单位： 北京大学

项目金额： 38万元

中文摘要： 本项目致力于构件组装正确性的研究，基于构件的开发方法在工业界中的应用越来越广，但是构件的理论研究仍然薄弱，以前的构件理论主要研究关于构件的形式化建模或基于服务质量的构件查找和组装方法究，特别是查找方法。本课题主要研究基于构件组装功能正确性的理论和方法。主要研究进展有：(1)在构件的形式化模型方面，以构件的进程代数模作为参照，提出了构件的多种Petri网模型及其建模方法。可以描述构件的多种属性，包括时间、角色等；(2)在构件互操作的种类及其建模方面，主要研究了构件的精化方法，给出了构件在四种层次上精化的定义及其性质；(3)在构件性质的时态逻辑描述和验证方面，改造了分离逻辑；给出了多种基于图（graph）算法的构件性质正确性证明算法，这是本项目的重点；（4）给出了一些基于上述正确性组装方法的构件查找启发式算法。总之，本项目较地好解决了构件组装正确性无法检查、无法判断问题，很好地完成了项目合同规定的研究任务。本项目已发表论文18篇，其中Theoretical Computer Scienc、IEEE Transaction系列杂志论文共3篇，接受待发表论文3篇。

中文关键词： 构件组装；模型验证；Petri 网；时态逻辑

英文摘要： This Project aims to investigate the correctness of component compositions. Rather discussing QoS aspects or looking-up methods of component compositions, we foucus on functional correctness of component compositios. The main progress we had made are in the following four aspects. (1) For the formal modeling of components, comparing with process algebra model of components, we define verious models, based on Petri Nets, to decribe verious aspects of components, including timing and role in components. (2) For the interoperation among components, we focus on the refiments of two components. Four issues of component refinments has been investigated. Their poperties are also discussed. (3) For the description and verification of temporal properties of components, we modify seperation logic so that the logic is adaptive for description and verification. Some model checking problem of correctness of component compositions are reduced to graph- theoretical problem，and corresponeding algorithms are given. (4) Some heuristic looking-up algorithms are also given base on the above thchniques. We accomplish the task well the project aggrement assigned.

英文关键词： component composition; model checking;Petri Net; Temporal Logic