| 基于SPIN的G语言系统模型的验证 |
| |
| 引用本文： | 薛艳,武淑红,王耀力.基于SPIN的G语言系统模型的验证[J].计算机科学,2018,45(Z6):536-540, 544. |
| |
| 作者姓名： | 薛艳 武淑红 王耀力 |
| |
| 作者单位： | 太原理工大学计算机科学与技术学院 山西 晋中030600,太原理工大学计算机科学与技术学院 山西 晋中030600,太原理工大学信息工程学院 山西 晋中030600 |
| |
| 基金项目： | 本文受山西省自然科学基金资助 |
| |
| 摘 要： | 对于大型系统,为确保其运行的可靠性、稳定性及高效性,需要从两个方面对系统进行验证:业务模型和系统模型。目前,对业务模型的验证可通过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 |
| 作者简介： | 薛 艳(1991－),女,硕士生,主要研究方向为编译器相关技术及应用、嵌入式开发、AI,E-mail:617989449@qq.com；武淑红(1969－),女,博士,副教授,主要研究方向为计算机应用、音视频编码算法、金融信息系统设计以及SoC与嵌入式系统软、硬件技术研究；王耀力(1965－),男,博士,副教授,主要研究方向为信息系统设计、人机视觉分析与处理、嵌入式系统电路设计理论。 |
| |
Verification of G Language System Model Based on SPIN |
| |
| XUE Yan,WU Shu-hong and WANG Yao-li.Verification of G Language System Model Based on SPIN[J].Computer Science,2018,45(Z6):536-540, 544. |
| |
| Authors: | XUE Yan WU Shu-hong WANG Yao-li |
| |
| Affiliation: | Department of Computer Science and Technology,Taiyuan University of Technology,Jinzhong,Shanxi 030600,China,Department of Computer Science and Technology,Taiyuan University of Technology,Jinzhong,Shanxi 030600,China and Department of Information Engineering,Taiyuan University of Technology,Jinzhong,Shanxi 030600,China |
| |
| 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. |
| |
| Keywords: | System model G language SPIN G2Promela SPOG |
|
|
|
|
下载PDF全文