实时系统是面向方面技术很好的应用场所,在实时系统中,有很多非功能需求,且这些非功能需求往往横切整个系统。在实时系统中关键的就是时间要求了,这些时间要求散布在整个系统的功能部件里,带来了代码混乱和代码分散问题。　　 实时系统的复杂性的不断增加以及对可配置性和可重用性要求的不断提高,需要如面向方面和基于组件的软件工程方法的支持,同时实时系统的可信性要求采用形式化方法来开发实时系统。本文试图建立一种面向方面的实时系统形式化开发方法,这种方法对RT-Z的进行了面向方面和面向部件的扩展,并通过实时组件模型在需求和设计阶段提供了对基于部件的系统开发方法(CBSD)和面向方面的系统开发方法(AOSD)的支持。本文给出了面向方面的实时Z(AO-RT-Z)的组件模型的框架结构、语法要求、方面的联结和功能接口和非功能接口的定义,重点讨论并证明了面向方面的实时Z(AO-RT-Z)作为规格描述语言的健全性。　　 形式化方法是建立在严格的数学基础上的,具有精确数学含义的科学研究和验证方法。可信分布式实时系统开发过程中的时间分析是非常复杂的,涉及到不同的方面,需要考虑很多东西,不同的可信分布式实时系统具有不同的时间性需求,不能用一种开发方法进行分析、设计和实现。由于形式化方法具有严谨、可数学分析、证明、完整性、一敌性、无二义性和精确性等特性,可以根据系统开发的不同方面采用不同的形式化语言进行分析、设计和实现,然后再把这些方面编织应用到系统中去,来完成它在系统中特定的作用。因此形式化方法已经成为人们深入研究的一个领域。　　 本文主要研究将面向方面的形式化方法技术用于可信分布式实时系统机制研究。首先系统性地介绍了可信分布式实时系统、UML、QoS和面向方面开发方法等相关技术,为本文限定了研究范围；然后深入研究了时间模型及面向方面建模；随后结合相关的关键技术和数学思想,给出了几种面向方面的形式化分析方法。最后总结了本文的研究工作,指出了下一步的研究方向。