Formal Verification for AltaRica3.0 Models Based on SPIN
Proceedings of 2017 the 7th International Workshop on Computer Science and Engineering · 2017
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.0model.The main work of this article is to analyze the AltaRica3.0model 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.0flattening to a GTS model, the core conversion rules of the AltaRica3.0model 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.0model 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.