计算机科学与探索2017，Vol.11Issue(1)：24-36,13.DOI:10.3778/j.issn.1673-9418.1511003
面向AltaRica模型的嵌入式系统安全性验证方法
Safety Verification Methodology of Embedded System Based on AltaRica Model
摘要
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.关键词
嵌入式系统/安全性验证/AltaRica模型/Promela模型Key words
embedded system/safety verification/AltaRica model/Promela model分类
信息技术与安全科学引用本文复制引用
仵志鹏,胡军,陈松,石娇洁..面向AltaRica模型的嵌入式系统安全性验证方法[J].计算机科学与探索,2017,11(1):24-36,13.基金项目
The National Basic Research Program of China under Grant No.2014CB744903(国家重点基础研究发展计划(973计划)) （国家重点基础研究发展计划(973计划）
the Scientific Research Foundation for the Returned Overseas Chinese Scholars,State Education Ministry of China under Grant No.2012 (教育部回国留学人员科研启动基金) （教育部回国留学人员科研启动基金）
the Science Foundation for Youth Science and Technology Innovation of Nanjing University of Aeronautics and Astronautics under Grant No.NS2014098(南京航空航天大学青年科技创新基金). （南京航空航天大学青年科技创新基金）
