一种面向同步反应式构件的软件架构模型正确性验证方法

本发明公开了一种面向同步反应式构件的软件架构模型正确性验证方法，涉及模型验证技术领域，在本发明中借助Dom4j包解析XML格式的源模型，提取并分类存储模型结点、迁移及全局变量信息。然后，设计从软件架构模型到PROMELA代码的映射规则，涵盖模型结构、数据及各类元素的转换。利用SPIN工具定义安全性和活性验证属性，通过控制变量与断言判断控制结点分支可达性。从开始节点起，将模型元素顺序转换为PROMELA的变量、通道和进程。最后，生成验证脚本，对转换后的模型进行语法检查与属性验证，解析验证报告获取结果，若需验证其他属性可重复操作。该方法为确保软件架构模型的正确性提供了系统、有效的手段。