Research On Transformation And Verification Of G Language System Model

G language is a programmatic block diagram language based on data flow.There are many kinds of fully encapsulated algorithm modules inside,and its application field is very wide.Currently,G language is not listed in the ANSI standard language and is used in conjunction with NI(National Instruments)hardware.In order to retain the existing algorithm modules and mature algorithms that have been applied in the products and reduce the price of the hardware products,it is necessary to convert the G language into an international standard language to be compatible with the general hardware platform.ANSI-C is the most popular language in the field of embedded development and can be applied to a variety of hardware products.Therefore,designing and implementing a G2ANSI-C system model transformation platform that can extend the application scope of G language,and achieve the decoupling of hardware and software is one of the problems that need to be solved.At present,smart products developed in G language are increasingly entering people's lives.Therefore,higher requirements are placed on the reliability and security of products.When using the G language for system design,it involves a procedural block diagram that controls the background logic and a front panel that interacts with people.It is difficult to read and check it,and there is no tool to detect it.In general,the detection of the system can use manual code exercises,peer review,static source code analysis,simple old units and integration tests.These methods are effective in capturing errors,but their detection efficiency is low.Therefore,it is necessary to use the automated verification tool SPIN to perform the verification of the G language system.That is to say,achieving G2 Promela is the second problem to be solved.This article designed and implemented G2ANSI-C and G2 Promela.Its technical framework uses the compiler's three-tiered classical architecture,frontend-midend-backend,and undergoes a series of improvements and optimizations.In the implementation of the overall system,G2ANSI-C and G2 Promela share a frontend,and the midend performs the optimization based on the created G2 ANSI-C and G2 Promela mapping tables.The backend is the output of the G2 ANSI-C and G2 Promela optimization results,respectively.In the frontend design,the FA algorithm and the regular expression theory are mainly used to complete the acquisition of the Token set,and the grammar rules are designed using the improved BNF paradigm.The improved algorithm LALR(1)is used to perform the grammar analysis and construct AST,where the construction of the analysis tables is the focus of research.In the research process of the project,the G2ANSI-C mapping table and the G2 Promela mapping table were created by analyzing the rules of the three languages.Based on these two tables,the optimization work for the midend is separately classified and implemented.In the G2ANSI-C transformation,the middleend adopts the DFS depth-first algorithm to traverse the abstract syntax tree,completing the optimization of keyword substitution,redundant code elimination,operator processing,IO flow variable identification,and black box conversion of the adjusted function.In the transformation of G2 Promela,in order to ensure that the main logic of the G language remains unchanged,optimizations are made in terms of keywords,variables,method functions,basic structures,and pointers,so that each Token of the G language complies with Promela's specifications,and thus successfully built.The mold is verified.In the output stage of the target code,under the same module HeaderCodeGen,the leaf nodes are sequentially obtained using the DFS traversal method,and are output to the file with the.pml suffix.After acquiring the generated target code ANSI-C,use the Modex tool to model it and use the SPIN tool to automate it.After acquiring the Promela model,verify it directly in the SPIN tool.The verification process includes six stages including Syntax Check,Redundancy Check,Symbol Table,Automata View,Simulate Replay,and Verification.The model includes model anomalies,process flow,running time,deadlock,storage capacity,and reachable path depth.Finally,through the analysis of the results,it is concluded that the generated ANSI-C program indexes are superior to those extracted directly from the G language,and the validity of the model conversion and verification constructed system is verified.Based on the system constructed in this paper,the decoupling of the G language platform can be realized,and the application scope of the G language can be extended.At the same time,it provides an automatic verification method for the G language,which has a strong theoretical and practical value.