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

随着软件产业的迅速发展，基于构件的开发方法在工业界中的应用越来越广泛，构件可能成为下一代软件的基本形态。但是构件的理论研究仍然薄弱，大部分现有的构件理论研究工作都是关于构件的形式化建模或基于服务质量的构件查找和组装方法研究。本课题的重点在于深入研究保证构件组装功能正确性的理论和方法，所用的方法是以Petri网为建模工具、以时态逻辑为性质描述语言来自动验证或半自动验证构件组装性质的正确性。基于构件组装正确性的验证方法，还可以深入探索可靠的构件发现、组装技术。研究内容包括:(1)构件的形式化模型；(2)构件之间互操作的种类及其建模；(3)构件性质的时态逻辑描述；(4)构件性质正确性的推导证明方法及模型检查算法；(5)基于正确性的构件查找策略及组装方法。本项目的成果可为基于构件的开发方法提供坚实的理论基础，为构件的可靠性提供的一种关键技术，并可能为构件的发现、组装提供新的方法。