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

注：因版权方要求，不能公开全文，如需全文，请咨询杂志社