基于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语言程序的性能.

关键词：系统模型、G语言、SPIN、G2Promela、SPOG

所属期刊栏目：45

分类号：TP399(计算技术、计算机技术)

资助基金：山西省自然科学基金

在线出版日期：2018-08-15（万方平台首次上网日期，不代表论文的发表时间）

页数：共6页

页码：536-540,544