应用在航天航空、轨道交通等安全关键领域的嵌入式系统,不仅要求硬件系统运行可靠,对嵌入式软件可靠性安全性也提出了更高的要求。尽早开展需求建模分析与验证,可以最大程度上规避需求偏离的风险,降低后期软件错误纠正的成本。形式化方法以严格的数学化和机械化方法为基础来规约、构建和验证计算机系统。因此,形式化验证已逐步成为被广泛接受、认可的解决方法。针对目前存在的形式化建模低效、准确性差的问题,本文开展了嵌入式软件需求自动建模技术研究。针对安全关键领域软件潜在攻击风险等问题,本文以CAN总线为对象,开展了基于可变攻击者的CAN总线系统健壮性验证技术研究。从而提升形式化验证方法在工程中使用。在需求自动建模方面,首先开展了模型转换算法的研究,为数据流图（Data Flow Diagram,DFD）添加时间约束属性,设计元素映射规则,提出了一种数据流图转换为时间自动机（Timed Automata,TA）模型的DFD-TA算法,并进行了实际应用中的模型转换与验证。其次,本文构建了一套可复用的航天嵌入式软件通用接口协议的模板库与验证知识库,包括常用的CAN总线、1553B总线、LVDS接口等协议,使用模板库可快速进行相似场景下的软件需求形式化建模,提高了建模的效率和验证有效性。在CAN总线健壮性验证研究方面,提出了一种基于UPPAAL SMC的CAN总线健壮性分析验证方案,将神经网络与形式化方法相结合。首先基于循环神经网络（Recurrent Neural Network,RNN）和长短时记忆网络（Long-Short Term Memory,LSTM）实现了CAN总线攻击报文的生成,提出了一种将神经网络模型转换为时间自动机模型的DL-TA算法,实现了RNN到TA的形式化模型转化,构建了可变攻击者模型Auto Attacker。其次,构建了基于可变攻击者的CAN总线数据链路层与应用层的综合模型,开展了CAN总线抗攻击者入侵健壮性影响评估。开发人员可根据评估结果改进软件需求关键参数指标。实验结果表明,参数优化后,在总线被攻击情况下节点传输准确率提升了2.5%,应答正确率提升了5.1%,加强了总线抗攻击能力。该方法为嵌入式软件通讯总线系统设计的合理性提供了理论指导,规避开发后期的风险。