嵌入式系统是复杂的反应式系统,其主要特点是持续与外部环境进行交互、运行通常没有终止状态。由于嵌入式系统本身的确定性、并发性、实时性,对此类系统进行形式化建模具有很大的挑战性;进一步地,验证嵌入式系统模型是否满足可靠性、安全性、活性等关键属性具有十分重要的意义。　　UML是工业上软件建模事实上的标准语言,它的多种视图为嵌入式系统的结构、行为建模提供了便利:组件图是工业上普遍采用的一种描述嵌入式系统静态结构的可视化方法,它将复杂的系统划分为多个组件并且描述了这些组件之间的交互依赖;此外,还可以使用体系结构描述语言对其进行形式化描述。Statecharts是工业上广泛采纳的一种嵌入式系统行为建模的形式化方法,它描述了系统中的状态以及状态之间的变迁,它的运用为系统行为的形式化验证奠定了基础。但是这两种视图均没有分离嵌入式系统中的核心模块与横切模块,使得横切模块交织、散布在核心模块中,导致了嵌入式系统的开发效率低、系统的可维护性以及可扩展性差等一系列问题。　　面向方面是建立在面向对象软件开发基础上并对其进行扩展的一种新型软件开发方法。本文对UML进行面向方面的扩展,结合UML和面向方面的优点对嵌入式系统进行形式化建模。本文的研究思路为:面向方面需求分析-面向方面软件架构-面向方面软件建模-模型验证-系统实现。具体研究成果主要分为以下几个部分:　　提出了一种基于用例的面向方面建模方法,从而在系统开发的最初阶段实现关注点的有效分离。嵌入式系统需求被划分为功能需求和非功能需求,功能需求进一步细化为核心功能需求、被包含功能需求、扩展功能需求以及继承功能需求。其中,核心功能需求被描述为基本用例模型,而其它三类需求则被描述为方面用例模型。非功能需求主要用于描述与系统性能相关的关注点,如日志、安全、响应时间等,该类需求也被描述为方面用例模型。此方法为嵌入式系统的结构分析和行为分析提供了基础。　　提出了一种新型的面向方面软件体系架构(AOSA)。由于面向方面体系架构包括结构分析和行为分析两部分,定义了一种基于XML的面向方面体系结构描述语言(XAOADL)描述系统的结构部分。通过形式化地定义体系架构、组件、方面、连接件以及编织器,有效实现了嵌入式系统的结构分析。　　对于面向方面体系架构中的行为分析,引入面向方面Statecharts(AOSC)形式化描述架构中组件之间、组件与方面之间的交互行为。给出了基本Statecharts和方面Statecharts的定义,通过具体算法实现了两者的编织;编织后的AOSC被转化为扩展层次自动机(EHA)实现模型的结构化表示,从而解决了AOSC中存在的层问迁移问题;进一步通过标签迁移系统(LTS)描述EHA模型的操作语义,使用线性时态逻辑描述系统的关键属性,最后通过模拟系统的执行路径实现对嵌入式系统行为的分析与验证。　　提出了一种嵌入式系统界面组件的面向方面设计方法,使用动态链接库描述系统的核心关注点,使用AspectC++实现系统的横切关注点,从而根据需要动态加载系统核心模块及横切模块,进一步提高小型嵌入式系统的模块化程度,有效缓解嵌入式系统资源受限的问题。