科研之友
微信
新浪微博
Facebook
分享链接
摘要
自动检测与验证HMSC (high-level message sequence chart)模型的正确性对保证文本需求被正确建模具有十分重要的意义，为此提出一种为HMSC模型进行自动检验的方法，并将其实现。利用转换规则为HMSC模型生成Promela检测语言，借助SPIN工具对需求进行验证。该方法不仅支持模型检测，同时通过对系统行为的动态模拟可以实现需求的合理性分析。从Promela实现到SPIN验证整个过程实现自动化操作。在该方法的基础上实现一个文本需求自动建模及检测分析的工具，通过一个实例展示其自动建模检测分析的效果，表明了其有效性和实用性。
-
单位浙江理工大学; 无锡科技职业学院; 枣庄科技职业学院
