基于SPIN的HMSC模型自动检验方法  

Automatic verification method of HMSC model based on SPIN

作　　者：李立亚[1] 孙雨荷 马汉杰[2] 丁佐华[2] 黄鸿云 LI Li-ya;SUN Yu-he;MA Han-jie;DING Zuo-hua;HUANG Hong-yun(School of Artificial Intelligence,Wuxi Vocational College of Science and Technology,Wuxi 214000,China;School of Computer Science and Technology,Zhejiang Sci-Tech University,Hangzhou 310018,China;Library Multimedia Big Data Center,Zhejiang Sci-Tech University,Hangzhou 310018,China)

机构地区：[1]无锡科技职业学院人工智能学院,江苏无锡214000 [2]浙江理工大学计算机科学与技术学院,浙江杭州310018 [3]浙江理工大学图书馆多媒体大数据中心,浙江杭州310018

出　　处：《计算机工程与设计》2023年第10期3047-3055,共9页Computer Engineering and Design

基　　金：国家自然科学基金项目(62132014)。

摘　　要：自动检测与验证HMSC(high-level message sequence chart)模型的正确性对保证文本需求被正确建模具有十分重要的意义,为此提出一种为HMSC模型进行自动检验的方法,并将其实现。利用转换规则为HMSC模型生成Promela检测语言,借助SPIN工具对需求进行验证。该方法不仅支持模型检测,同时通过对系统行为的动态模拟可以实现需求的合理性分析。从Promela实现到SPIN验证整个过程实现自动化操作。在该方法的基础上实现一个文本需求自动建模及检测分析的工具,通过一个实例展示其自动建模检测分析的效果,表明了其有效性和实用性。Automatic detection and verification of the correctness of the HMSC(high-level message sequence chart)model is of great significance to ensure that the text requirements are modeled correctly.To this end,a method for automatic verification of HMSC model was proposed and realized.The Promela detection language for the HMSC model was generated using the conversion rules,and the requirements were verified with the help of the SPIN tool.This method not only supports model checking,but realizes rationality analysis of requirements through dynamic simulation of system behavior.The entire process from Promela implementation to SPIN verification is automated.Based on this method,a tool for automatic modeling,detection and analysis of text requirements was implemented,and an example was used to demonstrate the effects of automatic modeling,detection and analysis,which shows the effectiveness and practicability of this method.

关 键 词：模型检测 HMSC模型 SPIN工具 正确性验证 模型转换 Promela语言 形式化方法 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]