摘要
自动检测与验证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.
作者
李立亚
孙雨荷
马汉杰
丁佐华
黄鸿云
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)
出处
《计算机工程与设计》
北大核心
2023年第10期3047-3055,共9页
Computer Engineering and Design
基金
国家自然科学基金项目(62132014)。
