• 学术研究 •

### 面向AltaRica模型的嵌入式系统安全性验证方法

1. 1. 南京航空航天大学 计算机科学与技术学院，南京 210016
2. 南京大学 计算机软件新技术国家重点实验室，南京 210093
• 出版日期:2017-01-01 发布日期:2017-01-10

### Safety Verification Methodology of Embedded System Based on AltaRica Model

WU Zhipeng1, HU Jun1,2+, CHEN Song1, SHI Jiaojie1

1. 1. College of Computer Science and Technology, Nanjing University of Aeronautics and Astronautics, Nanjing 210016, China
2. State Key Laboratory for Novel Software Technology, Nanjing University, Nanjing 210093, China
• Online:2017-01-01 Published:2017-01-10

Abstract:  As the embedded system is widely used in the safety-critical fields such as aeronautics, astronautics and transportation, AltaRica is a kind of formal modeling languages for safety-critical systems. Modeling critical systems based on AltaRica model and the safety analysis upon this have become the industrial standard in Europe. This paper proposes a kind of embedded system safety verification method based on AltaRica model, which includes, firstly model the embedded system using AltaRica, then exhibit the transformation rules from AltaRica model to Promela model, at the same time do formal proofs on transformation rules, so as to acquire the Promela model of embedded system, and finally use SPIN, a model check tool, to analyze and verify it. This paper takes the control unit of wheel brake system as an example to verify this transformation rules and method.