ISBN: 978-981-11-3671-9 DOI: 10.18178/wcse.2017.06.063
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
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
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.