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

来源：计算机科学与探索杂志2017年第1期北京时间：

作者：仵志鹏，胡军，陈松，石娇洁

单位：1. 南京航空航天大学 计算机科学与技术学院，南京 2100162. 南京大学 计算机软件新技术国家重点实验室，南京 210093

摘要：嵌入式系统在航空、航天、交通等安全关键领域的使用愈加广泛，AltaRica是一种描述安全关键系统的建模语言，同时基于AltaRica模型的安全性分析已成为欧洲的工业标准。提出了一种面向AltaRica模型的嵌入式系统安全性验证方法，包括：使用AltaRica语言对嵌入式系统进行建模；给出AltaRica模型到Promela模型的转换规则；对转换规则进行形式化证明，得到嵌入式系统的Promela模型；使用模型检验工具SPIN进行安全性验证。通过机轮刹车系统中的机轮刹车控制单元进行实例分析，验证了转换规则的正确性和有效性。

关键词：嵌入式系统,安全性验证,AltaRica模型,Promela模型