嵌入式系统应用广泛,嵌入式软件规模和复杂度急剧上升,呈现出组件化、综合化的发展趋势。同时,物联网、工业控制、航空航天等领域对嵌入式软件的可靠性、安全性要求越来越高,如何提高嵌入式软件的安全性和可靠性成为长期被关注的关键问题。基于模型的系统工程（Model-Based Systems Engineering,MBSE）常用于开发大型嵌入式软件系统,以提高软件可靠性。其中常用的系统建模语言（System Modeling Language,SysML）用于支持系统工程中的需求分析和设计活动。但现有的SysML建模工具缺乏针对安全属性验证和演化过程一致性测试的自动化支持,使得现有的形式化验证手段难以有效应用于复杂嵌入式软件的SysML模型设计。针对以上问题,本文以面向复杂嵌入式软件SysML模型设计的安全属性验证和一致性测试方法为研究对象,研究并提出了一种基于输入输出迁移系统（Input-Output Transition System,IOTS）和安全迁移系统（Secure Transition System,STS）的组件化嵌入式软件模型数据流安全性验证方法和一致性测试方法,用来确保软件模型设计中不存在违反数据流安全属性的行为,并确认系统模型的实现与其模型规范一致。本文主要工作包括以下4方面:（1）设计并实现了SysML模型到输入输出迁移系统和安全迁移系统的自动转化算法。SysML行为模型到输入输出迁移系统的转换算法能够将半形式化的SysML顺序图自动转化为形式化的输入输出迁移系统,用于对嵌入式软件模型的一致性测试;SysML模型到安全迁移系统的转换算法能够从包含安全属性信息的SysML需求、结构和行为模型图提取信息并转化为安全迁移系统,用于对嵌入式软件模型的数据流安全性验证。（2）提出并实现了基于安全迁移系统的数据流安全属性验证方法。安全迁移系统是输入输出迁移系统的扩展,其中包含从SysML模型图捕获的安全属性信息和系统行为信息。实现的自动验证算法基于安全迁移系统之间的无干扰属性决定过程,验证系统模型不存在违反数据流安全属性的行为。（3）提出并实现了基于输入输出迁移系统的一致性测试方法。基于系统模型演化前后不同粒度的SysML行为模型,分别从代表系统规范和系统实现的SysML顺序图提取相应的输入输出迁移系统,然后使用测试用例生成算法和测试执行算法检测系统行为实现是否与系统行为规范一致,从而保证系统实现的正确性。（4）实现了相应的模型转化、安全属性验证和一致性测试工具,实现了转化、验证和测试过程的自动化。针对无人机飞控系统的飞行模式切换子系统设计模型进行的安全验证和测试结果说明了本文方案和工具的有效性和实用性。