可信分布式实时软件的非功能特性的连贯性分析、设计与验证

非功能特性在分布式实时软件的分析与设计过程中起到非常重要的作用。本项目致力于建立非功能特性的连贯性分析、设计和验证方法，以提高分布式实时软件的可信性。连贯性分析和设计要求非功能特性必须在软件研制生命周期的所有阶段都被考虑，贯穿于软件规约到软件维护，特别是验证和确认阶段。项目通过提出基于模型驱动架构（MDA）的连贯性的面向方面的形式化开发方法来处理非功能特性，所采用的思想是把面向方面模型抽象成为形式化框架，即非功能特性的不同属性能够利用形式化技术来建模，能够产生规约驱动的设计，进行形式化验证及需求水平上的设计重用。特别是提出实时特性的连贯性的形式化的分析、设计、实现及验证的方法，确保可信分布式实时软件的实时特性需求被满足。将通过一个分布式多媒体系统的开发来验证所提出方法的有效性。本项目的研究工作将提高可信实时软件研究的水平，具有重大的科学意义和广阔的应用前景。