随着嵌入式系统设计复杂程度的提高，如何保障嵌入式系统安全成为计算机领域和工程界所关注的重要问题。本项目以嵌入式系统安全保障为中心，研究嵌入式系统安全事件建模与优化计算，利用大数据方法和自适应技术给出安全事件的数据建模、滤波和预判；分析嵌入式设备安全事件之间的关联与因果关系，研究系统运行阶段其设备可能产生的故障和安全问题的原因，对故障进行定位和预报，为嵌入系统的安全运行提供保障；研究安全风险评估算法，利用攻击图技术和漏洞库信息建立嵌入式系统安全风险评估系统，提高系统应对各种突发攻击事件的能力；研究嵌入式系统形式化建模与自动检测技术，设计和研发模块建模与模型检测一体化自动检测工具，在设计阶段检查和保障嵌入式系统的安全性和可靠性；以列车网卡MVB为研究案例，用自动机对MVB和列车网络通信协议进行形式化建模，对该嵌入式系统和协议进行仿真和检测，自动生成和优化VHDL代码，完成可信列车网卡的设计

With the design complexity increasing of embedded system, how to guarantee the embedded systems security has become an important issue in the computer science and engineering technology. The security of embedded systems is focus in this project. The data of the embedded system security event will be modeled based on the big data method and adaptive approaches. The filtering and optimization are concerned for data model. The causal relationship between events associated with the security of embedded devices will be analyzed. We will investigate that the reason of the equipment faults and security problems are possible generated in the operation stage of an embedded system. The fault location will be fixed and predicted to provide security for an embedded system. The algorithm of safety risk evaluation will be established. Based on the attack graphs technology and the vulnerability database information a safety risk evaluation will be proposed to enhance the ability of the embedded system dealing with all kinds of unexpected attacks. Formal modeling and automatic verification technology will be studied for embedded systems. An automatic verification tool integrated both modeling and model checking is designed and developed. Security and reliability of an embedded system is checked and guaranteed in the design stage. As an application instance, we will model MVB by the formal method. The MVB as well as the train network communication protocol will be modeled by automata. The simulation and formal verification will be executed for the MVB system and protocols. Furthermore, VHDL codes for the hardware are generated automatically, then, the trust MVB will be designed with formal methods.