%0 Journal Article %A 仵志鹏 %A 胡军 %A 陈松 %A 石娇洁 %T 面向AltaRica模型的嵌入式系统安全性验证方法 %D 2017 %R 10.3778/j.issn.1673-9418.1511003 %J 计算机科学与探索 %P 24-36 %V 11 %N 1 %X 嵌入式系统在航空、航天、交通等安全关键领域的使用愈加广泛,AltaRica是一种描述安全关键系统的建模语言,同时基于AltaRica模型的安全性分析已成为欧洲的工业标准。提出了一种面向AltaRica模型的嵌入式系统安全性验证方法,包括:使用AltaRica语言对嵌入式系统进行建模;给出AltaRica模型到Promela模型的转换规则;对转换规则进行形式化证明,得到嵌入式系统的Promela模型;使用模型检验工具SPIN进行安全性验证。通过机轮刹车系统中的机轮刹车控制单元进行实例分析,验证了转换规则的正确性和有效性。 %U http://fcst.ceaj.org/CN/10.3778/j.issn.1673-9418.1511003