Affiliation of Author(s):计算机科学与技术学院/人工智能学院/软件学院

Journal:Int. Workshop Comput. Sci. Eng., WCSE

Abstract:AltaRica is a kind of modeling language for safety critical systems, AltaRica3.0 is its latest version. There is still no corresponding formal verification method to analyze and verify the AltaRica3.0 model. The main work of this article is to analyze the AltaRica3.0 model by using a model test tool SPIN to analyze the different characteristics of AltaRica3.0 in relation to the previous version. Considering the basic structure of the underlying model GTS, based on the idea of AltaRica3.0 flattening to a GTS model, the core conversion rules of the AltaRica3.0 model to Promela model and a conversion framework are proposed. Based on the case analysis of the wheel brake system (WBS) in civil aircraft, the AltaRica3.0 model was established, and the Promela model was generated by the conversion rule. According to the safety requirements of the wheel brake system in 4761, SPIN is used to verify the system security attributes formally.

Translation or Not:no

Date of Publication:2017-01-01

Co-author:Li, Wanqian,Wang, Mingming,Zhang, Weijun

Correspondence Author:HU Jun