中文摘要：

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