基于SPIN的G语言系统模型的验证

对于大型系统,为确保其运行的可靠性、稳定性及高效性,需要从两个方面对系统进行验证:业务模型和系统模型。目前,对业务模型的验证可通过BPMN来完成；对系统模型的验证可通过SPIN(Simple Promela Interpreter)工具执行。G语言是由NI公司创建的一种图形化程序框图语言,还未被加入ANSI标准,因此,文中第一步工作是提取G语言的形式、规则、文法等语言特性。由于SPIN对G语言不提供直接的支持,因此第二步工作是完成G2Promela的映射。在G2Promela的工作中,主要是基于编译器的框架,以Scanner-Parser-Optimizer-Generator(SPOG框架)为主线,根据第一步的预处理工作,按方法函数、指针、关键字、变量等分类创建G2Promela的映射规则,最终实现G2Promela的转换,完成对G语言系统模型的验证。该方法的提出弥补了G语言系统模型验证方面的空白,从而更深入地确保了G语言程序的性能。

Verification of G Language System Model Based on SPIN

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.