Abstract:

AltaRica language is used in safety critical systems modeling. It has a complete set of modeling analysis tools. However, with the AltaRica3.0 update, traditional AltaRica modeling and analysis tools like ARC are no longer supportive, and the SPIN as an exhaustive model verification tool is widely used. We briefly introduce the improvement of AltaRica3.0 over the previous version in terms of expressive ability and the basic structure of the underlying model GTS. Based on the idea of AltaRica3.0 flattening into the GTS model, we propose a conversion rule for AltaRica3.0 model transformation to the Promela model. Taking the civil aircraft wheel brake system (WBS) as an example, the AltaRica3.0 model is established and transformed into the Promela model by the conversion rule. Finally, according to the safety requirements of the WBS in 4761, the SPIN tool is used to verify the safety property of the WBS.

Key words: safety-critical system, AltaRica3.0, SPIN, wheel brake system