Abstract: For large systems,in order to ensure the reliability,stability and efficiency of its operation,it is necessary to verify the system from two aspects,the business model and the system model.At present,the validation of the business model can be done through BPMN.For the system model validation,SPIN tool is selected.G language created by the NI company is a graphical block diagram language and has not yet joined the ANSI standard.Therefore,the first step is to extract the G language form,rules,grammar and other language features.SPIN does not provide direct support for the G language,so the second step is to complete the G2Promela mapping.In the work of G2Promela,mainly taking the framework of the compiler to Scanner- Parser- Optimizer- Generator (SPOG framework) as the main line,according to the first step of the pre-processing work,G2Promela mapping rules is classified and created through the method function,pointer,keywords,variables to realize the G language system model validation.The proposed method complements the gaps in the G language system model validation,thus further ensuring the performance of the G language program.

Key words: G language, G2Promela, SPIN, SPOG, System model