WCSE

Formal Verification for AltaRica3.0 Models Based on SPIN

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.

Index Terms— safety-critical system, AltaRica3.0, SPIN, Wheel Brake System.

Hu Jun, Li Wanqian, Wang Mingming, Zhang Weijun
College of Computer Science and Technology, Nanjing University of Aeronautics and Astronautics, CHINA

[Download]

Cite: Hu Jun, Li Wanqian, Wang Mingming, Zhang Weijun, "Formal Verification for AltaRica3.0 Models Based on SPIN," Proceedings of 2017 the 7th International Workshop on Computer Science and Engineering, pp. 366-370, Beijing, 25-27 June, 2017.