随着硬件性能的快速提升,通信与网络的迅速发展,嵌入式系统及其应用不断涌现。嵌入式软件系统的复杂性也在迅速增长。软件在嵌入式系统中占据重要地位。如何利用现代软件工程的方法与技术,降低软件开发的复杂性、适应经常变化的客户需求、降低开发成本、提高软件可信性已经成为嵌入式软件开发领域的重要课题。将软件需求描述与特定平台的实现分离是实现缩短软件开发时间、适应不断变化的需求、降低开发成本的有效手段。模型驱动架构(Model Driven Architecture, MDA)是目前实现这一目标的最有吸引力的方法之一。在基于MDA的软件早期设计阶段,目标系统的可选方案可以做充分的检查和比较。软件的开发风险因而可以被降低。模型是基于MDA的软件开发过程中最主要的元素。UML已经是事实上的软件建模标准,并且被OMG推荐用来描述MDA中的建模。然而UML无法描述系统非功能属性。非功能属性在可信软件开发过程中非常重要。OMG最近针对嵌入式系统建模和分析的需要提出了MARTE Profile来描述嵌入式系统的非功能属性。本文将MARTE的Stereotype和标签值标注在UML模型的相关节点上。带MARTE标注的UML模型记为UML/MARTE。形式化方法是提高软件可信性的重要手段。为了形式化地描述嵌入式系统,本文给出了带抑止弧的时延着色Petri网(TCPNIA),并围绕TCPNIA给出了相应的模型验证与分析方法。为了在MDA的早期开发阶段利用TCPNIA形式化地验证和分析UML模型,文章给出了从UML/MARTE模型到TCPNIA模型的转换方法。本文的主要研究成果包括如下方面：(1)给出了在UML图形中利用MARTE Profile标注非功能属性的方法。通过在活动图与序列图中选择恰当的被标注节点,该方法可以实现层次化地标注UML图形,从而可以提高模型及相关验证结果的可重用性。给出了UML/MARTE模型元素的形式化定义,这为模型的形式化转换与分析奠定了基础。(2)提出了一种融合时延Petri网、着色Petri网和抑制弧的特征的模型TCPNIA,并在变迁中引入能量消耗特征和数据操作函数,给出了TCPNIA的形式化语法和语义。这一模型既可以实现对复杂系统的功能和非功能属性建模,又可以充分利用现有Petri网的分析技术。TCPNIA模型为利用Petri网建模与分析实时嵌入式系统提供了基础。(3)给出了从TCPNIA到时间自动机(Timed Automaton, TA)的转换算法。该算法引入变迁冲突调解机制,保证时延变迁语义在时间自动机中得到保持。本文的方法也适用于利用Uppaal验证一般时延Petri网。(4)给出了一种在时间和资源限制下的TCPNIA模型的任务调度算法。在计算时间消耗时考虑了路径中变迁的并行执行情况。为了提高模型分析结果的重用性和计算效率,本文分析了可调度路径的分解与组合分析方法。该算法采用递归的深度优先搜索方法,只需产生部分状态空间,从而在一定程度上减轻了状态爆炸问题。(5)分别以图形化和形式化语法方式给出了从UML/MARTE到TCPNIA的转换方法。该方法根据UML模型特征确定面向方面的切入点,并给出了自动生成方面的算法。在面向方面编织规则的基础上,给出了Petri网模型的自动组合算法。这些方法为开发从UML/MARTE到TCPNIA模型的自动转换工具提供了理论基础。