G语言是一种基于数据流的程序化框图语言,内部有多种完全封装的算法模块,其应用领域非常广。目前,G语言未列入ANSI标准语言,且与NI(National Instruments)硬件绑定使用。为了保留现有的算法模块及已经在产品中应用的成熟算法,并降低硬件产品的成本,有必要将G语言转化为某种国际标准语言,以兼容通用硬件平台。ANSI-C是一种在嵌入式开发领域最受欢迎的语言,可以应用于多种硬件产品。因此,设计实现一种G2ANSI-C系统模型转化平台,拓展G语言的应用范围,并实现软硬件的解耦是亟需解决的问题之一。目前,G语言开发的智能产品,越来越多地走入了人们的生活,故对于产品的可靠性和安全性就提出了更高的要求。采用G语言进行系统设计时,涉及控制后台逻辑的程序化框图和负责与人交互的前面板,对其进行阅读、检查时比较困难,且没有针对其进行检测的工具。一般地,对系统进行检测,可以利用手动代码演练、同行评审、静态源代码分析、简单的旧单元和集成测试等,这些方法虽然可以有效地捕捉错误,但它们检测的效率较低。因此,需要利用自动化验证工具SPIN对G语言系统进行系模型验证,即实现G2Promela是亟需解决的问题之二。本文设计并实现了G2ANSI-C和G2Promela。其技术框架采用编译器的三层经典架构进行的,即前端-中端-后端,并进行了一系列改进和优化。在整体系统的实现中,二者共享一个前端,中端完成了基于创建的G2ANSI-C与G2Promela映射表进行优化的工作,后端是分别对G2ANSI-C与G2Promela优化结果的输出。在前端设计中,主要利用了FA算法和正则表达式理论完成Token集的获取,利用改良的BNF范式完成了文法规则的设计,采用改进的算法LALR(1)进行了语法分析构建AST,其中分析表的构建是研究的重点。在课题研究过程中通过对三种语言的规则分析比对,创建了G2ANSI-C映射表以及G2Promela映射表。基于这两个表,对中端的优化工作分别进行分类实现。在G2ANSI-C的转化中,中端采用了DFS深度优先算法对抽象语法树遍历,完成了对关键字替换、冗余代码消除、运算符处理、IO流变量识别及被调函数黑盒转换的优化工作。在G2Promela的转化中,为保证G语言的主体逻辑保持不变,从关键字、变量、方法函数、基本结构及指针等方面进行优化,使G语言的各个Token都符合Promela的规范,从而成功建模完成验证。在目标代码的输出阶段,在同一个模块HeaderCodeGen下,采用DFS遍历方式依次获取叶子结点,并输出到.pml后缀的文件内。在获取生成的目标代码ANSI-C后,利用Modex工具进行建模,并采用SPIN工具对其进行自动化验证。在获取Promela模型后,直接在SPIN工具中进行验证。验证工作经过Syntax Check、Redundancy Check、Symbol Table、Automata View、Simulate Replay及Verification 6个阶段,包含模型异常、进程流程、运行时间、是否存在死锁、存储容量大小及可达路径深度等多项指标。最终,通过对结果的分析,得出生成的ANSI-C程序各项指标均优于直接从G语言提取的模型,验证了所构建的模型转换和验证系统的有效性。基于本文构建的系统,可以实现G语言平台的解耦,扩展了G语言应用范围,同时为G语言提供了自动化验证手段,具有很强的理论和实用价值。