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

软件模型检验的可扩展性是一个技术难点，它严重制约了模型检验技术在软件方面的广泛应用。针对此问题，本课题研究以组合的方式对软件系统进行形式验证，以扩大验证规模、提高验证能力。课题针对Java构件的关键性质在设计层和实现层统筹进行验证，可有效提高软件设计与实现阶段的质量保障能力。主要研究内容包括：Java构件设计层的组合模型检验技术、Java构件实现层的组合模型检验技术，包括两个层次验证的衔接和有效集成，同时开发相应的组合模型检验工具。本课题的研究能显著提高面向对象软件关键性质的保障能力，能丰富和发展形式验证理论，因而具有广泛的应用价值和重要的科学意义。