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

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

仵志鹏1，胡 军1,2+，陈 松1，石娇洁1

【摘 要】嵌入式系统在航空、航天、交通等安全关键领域的使用愈加广泛,AltaRica是一种描述安全关键系统的建模语言,同时基于AltaRica模型的安全性分析已成为欧洲的工业标准.提出了一种面向AltaRica模型的嵌入式系统安全性验证方法,包括:使用AltaRica语言对嵌入式系统进行建模;给出AltaRica模型到Promela模型的转换规则;对转换规则进行形式化证明,得到嵌入式系统的Promela模型;使用模型检验工具SPIN进行安全性验证.通过机轮刹车系统中的机轮刹车控制单元进行实例分析,验证了转换规则的正确性和有效性. 【期刊名称】计算机科学与探索 【年(卷),期】2017(011)001 【总页数】13

【关键词】嵌入式系统；安全性验证；AltaRica模型；Promela模型

WU Zhipeng,HU Jun,CHEN Song,et al.Safety verification methodology of embedded system based on Alta-Rica model.Journal of Frontiers of Computer Science and Technology,2017,11(1)：24-36.

1 引言

随着嵌入式系统在航空、航天、能源动力、铁路交通等领域的使用愈加广泛，系统失效可能造成人员伤亡，财产损失，甚至环境危害等可怕后果。因此保证嵌入式系统的安全性和可靠性已然成为软件工程领域研究的热点问题之一[1]。为提高嵌入式系统的安全性和可靠性，针对系统模型的安全性分析与验证已成为系统开发周期中的重要环节。