一种基于性质规约模式生成LTL公式的UML模型检测系统和方法

摘要

本发明涉及模型驱动式软件开发领域中一种基于性质规约模式生成LTL公式的UML模型检测系统和方法，其特征在于，包括：UML状态图、模型编辑器、模型转换器、模型检测器、LTL公式编辑器，基于性质规约模式自动生成LTL公式定义模板、并由用户定义配置该性质规约模板，最终将生成的LTL公式输入到所述模型检测器中，验证LTL公式，并对验证结果进行分析。在系统建模过程中，基于性质规约模式生成描述系统性质约束的LTL公式，并使用模型检测器验证UML状态图建模的系统动态行为是否满足LTL公式，检查UML模型是否满足系统所期待的性质约束，实现在建模阶段构造出高质量的系统模型，从而提高最终生成的软件系统的质量。