科研之友
微信
新浪微博
Facebook
分享链接
摘要
本发明涉及一种验证统一建模语言UML模型中动态行为与时序契约的一致性的方法,其特征在于,包括步骤：根据UML标准建模,包括生成UML状态图和UML顺序图,保存图形的元模型；对所建模型的动态行为,实现UML状态图到PROMELA代码的映射；构建所建模型时序契约,实现UML顺序图到LTL时态逻辑公式的映射；利用模型验证工具SPIN对所述PROMELA代码和所述LTL时态逻辑公式进行验证；分析返回的所述的SPIN验证结果。本发明的技术方案将统一建模语言UML同验证工具联系起来,解决了软件工程需求设计阶段所出现的模型不一致性的问题,为模型驱动式软件后续开发的有效进行奠定基础。
- 单位
