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

计算机科学 ›› 2018, Vol. 45 ›› Issue (6A): 536-540.

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

薛艳¹,武淑红¹,王耀力²

太原理工大学计算机科学与技术学院山西晋中030600¹
太原理工大学信息工程学院山西晋中030600²

出版日期:2018-06-20 发布日期:2018-08-03
作者简介:薛艳(1991－),女,硕士生,主要研究方向为编译器相关技术及应用、嵌入式开发、AI,E-mail:617989449@qq.com;武淑红(1969－),女,博士,副教授,主要研究方向为计算机应用、音视频编码算法、金融信息系统设计以及SoC与嵌入式系统软、硬件技术研究;王耀力(1965－),男,博士,副教授,主要研究方向为信息系统设计、人机视觉分析与处理、嵌入式系统电路设计理论。
基金资助:
山西省自然科学基金资助

Verification of G Language System Model Based on SPIN

XUE Yan¹,WU Shu-hong¹,WANG Yao-li²

Department of Computer Science and Technology,Taiyuan University of Technology,Jinzhong,Shanxi 030600,China¹
Department of Information Engineering,Taiyuan University of Technology,Jinzhong,Shanxi 030600,China²

Online:2018-06-20 Published:2018-08-03

摘要/Abstract

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

关键词: G2Promela, G语言, SPIN, SPOG, 系统模型

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.

Key words: G language, G2Promela, SPIN, SPOG, System model

中图分类号:

TP399

薛艳, 武淑红, 王耀力. 基于SPIN的G语言系统模型的验证[J]. 计算机科学, 2018, 45(6A): 536-540. https://doi.org/

XUE Yan, WU Shu-hong, WANG Yao-li. Verification of G Language System Model Based on SPIN[J]. Computer Science, 2018, 45(6A): 536-540. https://doi.org/

参考文献

[1]CATTEL T.Modeling and Verification of sC++ Applications[C]∥Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems.Lisbon,Portugal,LNCS,1384.
[2]KOREL B.Automated software test data generation[J].IEEE Transactions on Software Engineering,1990,16(8):870-879.
[3]HOLTZMAN G.The SPIN Model Checker,Primer and Refe- rence Manual[M].Addison-Wesley Professional,2001.
[4]CHAN W,ANDERSON R J,BEAME P,et al.Model checking large software specifications[J].IEEE Transactions on Software Engineering,1998,24(7):498-520.
[5]HOLZMANN G J.The model checker SPIN[J].IEEE Transac- tions on Software Engineering,1997,23(5):279-295.
[6]HOLZMANN G J,SMITH M H.A practical method for verifying event-driven software[C]∥Proceedings of the 21st International Conference on Software Engineering.ACM,1999:597-607.
[7]王大伟,张大方,缪力.一种自动化模型检测 ANSI-C 程序的实用方法[J].计算机工程与科学,2010,32(4):79-82.
[8]郭伟,缪力,张大方,等.基于 Spin 的 UML 状态图模型检查的设计与实现[J].计算机工程与应用,2008,44(10):43-47.
[9]高晓星,李晓霞,薛冰.基于 UML 和 SPIN 的软件安全模型验证[J].长沙大学学报,2013,27(5):69-71.
[10]舒良春,饶俊,肖美华,等.基于 Promela 的 UML 建模方法及其应用[J].计算机与现代化,2010,2010(2):101-104.

相关文章 15

[1]	宋岚,薛锦云,胡启敏,谢武平,江东明,游珍. 无线射频RFID识别协议自动验证方法研究 Research of Automatic Verification Method about Radio Frequency Identification Protocol 计算机科学, 2017, 44(9): 99-104. https://doi.org/10.11896/j.issn.1002-137X.2017.09.020
[2]	陈光颖,黄志球,陈哲,阚双龙. 面向DO-333的襟缝翼控制单元安全性分析 Safety Analysis of Slat and Flap Control Unit for DO-333 计算机科学, 2016, 43(5): 150-156. https://doi.org/10.11896/j.issn.1002-137X.2016.05.028
[3]	肖美华朱科马成林. 基于SPIN的Andrew Secure RPC协议并行攻击模型检测 Model Checking of Parallel Attack in Andrew Secure RPC Protocol Based on SPIN 计算机科学, 2015, 42(7): 103-107. https://doi.org/10.11896/j.issn.1002-137X.2015.07.022
[4]	陈瑛,陈钊滢,叶小平. M-相点数据索引SPindex SPindex:Spatial Index Based on M-phase Points 计算机科学, 2015, 42(1): 206-209. https://doi.org/10.11896/j.issn.1002-137X.2015.01.046
[5]	程燕. 基于Cycle-spinning的多帧图像Contourlet去噪 Cycle-spinning Based Contourlet Denoising for Multiple Image 计算机科学, 2013, 40(Z11): 314-317.
[6]	崔海春欧阳丹彤王晓宇纪树平. 一种基于模式的故障诊断方法 Approach of Fault Diagnosis Based on Patterns 计算机科学, 2012, 39(11): 160-164.
[7]	钟勇,郭伟刚,钟昌乐,刘凤玉,李宁. Datalog逻辑程序调用语义及其应用研究 Research on Call Semantic of Datalog Logic Program and its Application 计算机科学, 2010, 37(1): 170-175.
[8]	王颖郑雪峰刘海燕. 一种鲁棒的三维水印方案计算机科学, 2009, 36(6): 262-264.
[9]	. 基于剪切不变的递归Contourlet变换图像去噪计算机科学, 2009, 36(5): 254-256.
[10]	李忠俊,周启海,帅青红. 一种基于内容和协同过滤同构化整合的推荐系统模型 Recommender System Model Based on Isomorphic Integrated to Content-based and Collaborative Filtering 计算机科学, 2009, 36(12): 142-145.
[11]	戴航,慕德俊,王林,张慧翔. Internet拥塞控制系统在不同源控制算法作用下的资源竞争分析 Analysis of Resource Competition for Internet Congestion Control Systems with Different Deployment of Source Algorithms 计算机科学, 2009, 36(11): 40-42.
[12]	敬超,常亮,古天龙. 基于SPIN的无线传感器网络安全协议建模与分析 Using SPIN to Model and Analyze Security Protocol in Wireless Sensor Network 计算机科学, 2009, 36(10): 132-136.
[13]	. LINUX进程间通信的模型检测计算机科学, 2008, 35(10): 295-299.
[14]	戎玫. SPS系统的一种精确语义描述计算机科学, 2008, 35(10): 284-287.
[15]	. 线性组合预测模型及其应用计算机科学, 2006, 33(9): 191-194.

Metrics

Viewed

Full text

Abstract

Cited

Shared

Discussed