论文部分内容阅读
AltaRica语言用于安全关键系统的建模,其拥有一套完整的建模分析工具,但随着AltaRica3.0的更新,ARC等传统的AltaRica建模分析工具已不再支持,而SPIN作为一个穷尽式模型验证工具被广泛应用。介绍了AltaRica3.0相对于之前版本在表达能力方面的改进,以及其底层模型GTS的基本结构。以AltaRica3.0扁平化为GTS模型的思想为基础,提出了一种AltaRica3.0模型向Promela模型的转换规则。以民用飞机中机轮刹车系统WBS为例,建立了AltaRica3.0模型,并且通过转换规则转为Promela模型。最后根据民用航空标准SAE ARP 4761中对机轮刹车系统的安全性要求,利用SPIN工具对机轮刹车系统的安全属性进行了验证。
The AltaRica language is used to model safety-critical systems with a complete set of modeling and analysis tools, but as AltaRica 3.0 is updated, traditional AltaRica modeling and analysis tools such as ARC are no longer supported and SPIN as an exhaustive Model verification tools are widely used. The improvement of AltaRica3.0 in terms of expression ability and the basic structure of its underlying model GTS are introduced. Based on the idea of flattening AltaRica3.0 into GTS model, a transformation rule of AltaRica3.0 model to Promela model is proposed. Taking WBS brake system in civil aircraft as an example, the AltaRica3.0 model was established and converted to Promela model by conversion rules. Finally, according to the safety requirements of the wheel brake system in the civil aviation standard SAE ARP 4761, the safety properties of the wheel brake system are verified by using the SPIN tool.