Java构件的组合模型检验技术研究

项目名称： Java构件的组合模型检验技术研究

项目编号： No.60803042

项目类型： 青年科学基金项目

立项/批准年度： 2009

项目学科： 金属学与金属工艺

项目作者： 文艳军

作者单位： 中国人民解放军国防科学技术大学

项目金额： 20万元

中文摘要： 软件模型检验的可扩展性是一个技术难点，它严重制约了模型检验技术在软件方面的广泛应用。针对此问题，本课题研究以组合的方式对软件系统进行形式验证，以扩大验证规模、提高验证能力。课题针对Java 构件的关键性质在设计层和实现层进行验证，可有效提高软件设计与实现阶段的质量保障能力。本课题研究工作主要包括在构件设计层的基于Fractal构件模型的构件建模和分析、基于cCSP的构件语义模型研究、构件实现层的数据竞争和原子性问题的模型检验、Java构件运行时验证几个方面。本课题的研究能显著提高面向对象软件关键性质的保障能力，能丰富和发展形式验证理论，因而具有广泛的应用价值和重要的科学意义。

中文关键词： 组合模型检验；面向对象程序；形式验证；Fractal构件模型

英文摘要： How to improve the scalability of software model checking is a technical difficulty, which restrains the abroad application of model checking technology on softwares. As to this problem, the project focuses on the formal verification of software systems in a compositional manner, which can improve the scalability of formal verification. The verification problem of Java components at both design and implementation phases will be researched, which can effectively improve the quality assurance ability to software designs and implementations. The main research content includes: component modeling and analysis based on the Fractal component model, component semantics model based on cCSP, model checking of data-race and atomicity problem, runtime verification of Java components. The project can bring benefits to the quality assurance of objectoriented softwares on cricital properties, can enrich and develop the formal verification theories, and thus has abroad application value and important scientific meaning.

英文关键词： compositional model checking; object oriented programs; formal verification; Fractal component model