近年来随着嵌入式系统硬件性能的不断提高,嵌入式系统中软件的规模和复杂性也不断增加,软件对整个系统的影响逐渐占据了统治地位,从而使得嵌入式软件设计以及可靠性保障变得越来越困难。传统的嵌入式软件设计方法已经逐渐难以满足现代嵌入式软件设计的高可靠性需求,必须结合主流软件工程中处理复杂软件系统所采用的理论、技术与方法,如构件化设计、模型驱动架构、形式化规约与验证等。目前,模型驱动的嵌入式软件设计方法已经成为嵌入式计算领域中的研究热点。形式化方法是以数学为基础的用以对系统进行规约、设计和验证的语言、技术和工具的总称。对于具有高可靠性需求的嵌入式软件系统而言,建立有效的形式化验证技术具有非常重要的意义。因此,在嵌入式软件需求规约阶段引入形式化方法,并根据需求规约生成保留形式化语义的软件体系结构模型,可以极大提高嵌入式软件设计的可靠性。本文主要围绕嵌入式软件需求规约到软件体系结构模型转换的问题展开研究。重点研究了需求规约到软件体系结构模型的转换框架、基于MDE的LOTOS规约到UML-RT模型的转换方法、TCSP规约到UML-RT模型的转换方法、支持硬实时分析的进程代数规约与转换、支持资源分析的进程代数规约与转换问题。主要内容如下:(1)针对根据自然语言规约建立的软件体系结构模型的不精确性以及二义性问题,基于已有的自然语言规约到形式化规约的转换工作,提出了嵌入式软件需求规约到软件体系结构模型的转换框架,并在此基础上进一步提出了基于MDE的形式化规约到软件体系结构模型的转换框架。基于转换框架生成的软件体系结构模型保留了形式化语义,能够从本质上提高嵌入式软件软件体系结构设计的可靠性。(2)针对嵌入式软件时序规约到软件体系结构模型的转换问题,提出了基于MDE的LOTOS规约到UML-RT模型的转换方法。UML-RT是OMG组织专门针对实时与嵌入式系统软件体系结构建模的规范,然而基于自然语言规约建立的UML-RT模型往往是不精确的、存在二义性。为了使得UML-RT建模结果更为精确,需要赋予UML-RT模型形式化语义。LOTOS是一种适合于描述与验证嵌入式软件时序规约的进程代数方法。在需求规约到软件体系结构模型的转换框架下,使用LOTOS描述嵌入式软件时序规约,通过建立LOTOS到UML-RT的转换机制,实现了LOTOS规约到UML-RT模型的转换。实例分析表明该方法能够提高嵌入式软件软件体系结构设计的可靠性。(3)针对嵌入式软件实时规约到软件体系结构模型的转换问题,提出了TCSP规约到UML-RT模型的转换方法。时间通信顺序进程TCSP是进程代数通信顺序进程CSP的实时扩展,适合于描述与验证嵌入式软件的实时规约。在需求规约到软件体系结构模型的转换框架下,使用TCSP描述嵌入式软件实时规约,通过建立TCSP到UML-RT的转换机制,实现了TCSP规约到UML-RT模型的转换。实例分析表明通过该方法建立的UML-RT模型能够从整体上提高嵌入式软件软件体系结构设计的可靠性。(4)针对嵌入式软件缺乏有效的硬实时规约与验证机制,研究了支持硬实时分析的进程代数方法。通过扩展进程代数TCSP的硬实时语义,提出了硬时间通信顺序进程HTCSP,使之能够规约与验证嵌入式系统的硬实时动态行为。提出了时间最优调度算法,该算法有助于嵌入式系统硬实时的量化分析和优化设计。进一步给出了HTCSP规约到UML-RT模型的转换方法。(5)针对嵌入式软件缺乏有效的资源规约与验证机制,研究了支持资源分析的进程代数方法。通过扩展进程代数CSP的资源语义,提出了资源通信顺序进程RCSP,使之能够规约与验证嵌入式系统包含多种资源信息的动态行为。提出了资源优化检查算法,检查结果有助于嵌入式系统资源的量化分析和优化设计。最后讨论了RCSP规约到软件体系结构模型的转换方法。