摘要
本发明提供一种基于SysML模型的形式化验证系统，涉及软件工程技术领域。该基于SysML模型的形式化验证系统，包括模型管理模块、性质管理模块、映射配置模块和模型验证模块；所述模型管理模块，用于管理输入的SysML活动图模型；所述映射配置模块，用于SysML活动图的变量映射到形式化性质规约中的原子命题；所述模型验证模块，用于根据SysML活动图变量和形式化性质规约原子命题的映射，调用模型求解器，对Uppaa l模型进行验证，并返回验证结果。通过SysML活动图描述系统的行为和逻辑流程，再利用Uppaa l进行形式化的模型建立和分析，最终通过模型检查验证系统模型是否满足特定的性能和安全要求，从而确保系统设计的可靠性和有效性，提高了验证效率和降低了成本。
