|
|||||
|
|
| 面向AltaRica模型的嵌入式系统安全性验证方法 | |
| 作者单位： | ;1.南京航空航天大学计算机科学与技术学院;2.南京大学计算机软件新技术国家重点实验室 |
| 摘 要： | 嵌入式系统在航空、航天、交通等安全关键领域的使用愈加广泛,Alta Rica是一种描述安全关键系统的建模语言,同时基于Alta Rica模型的安全性分析已成为欧洲的工业标准。提出了一种面向Alta Rica模型的嵌入式系统安全性验证方法,包括:使用Alta Rica语言对嵌入式系统进行建模;给出Alta Rica模型到Promela模型的转换规则;对转换规则进行形式化证明,得到嵌入式系统的Promela模型;使用模型检验工具SPIN进行安全性验证。通过机轮刹车系统中的机轮刹车控制单元进行实例分析,验证了转换规则的正确性和有效性。 |
| 关 键 词： | 嵌入式系统 安全性验证 AltaRica模型 Promela模型 |
Safety Verification Methodology of Embedded System Based on AltaRica Model |
|
| Abstract: | |
| Keywords: | |