题目：基于谓词逻辑的机载嵌入式软件模型一致性检查技术研究

大型民用飞机是一个庞大的系统，其中机载嵌入式系统控制着从飞控、雷达到引擎在内的所有关键系统，是飞机的核心技术之一。在模型驱动的嵌入式软件开发中，模型的质量决定了软件产品的质量。建立一个系统的模型，必然要从不同的角度对系统进行静态的或动态的描述。如果模型中不同的视角对系统的描述相互矛盾，基于这个模型就不能建立一个可满足的系统，开发人员按照不一致的模型进行开发将造成严重的损失。因此在早期的设计阶段通过某种一致性验证方法找出系统行为的不一致之处，对于减少测试与维护的开销有着重要的意义。UML(Unified Modeling Language，统一建模语言)作为一种已经达到广泛应用的通用建模语言，同样在机载嵌入式软件开发领域得到普遍应用。现有的模型一致性检查的方法中，一类是将UML模型转换成其他类问题，这类方法可扩展性差。另一种基于谓词推理的方法可以有针对性地定义一致性约束，但是在现有的研究中多数是用来检查模型相对系统需求的一致性。本研究选用基于谓词逻辑的一致性检查方法，检查机载嵌入式软件UML模型视图间的一致性。本研究内容包括：定义UML元模型、设计UML模型信息到谓词逻辑的转换体系、使用谓词逻辑公式定义多组一致性检查规则并为每个规则提供实例验证。基于语义上的一致性检查理论，设计实现嵌入式软件模型一致性检查工具（Embedded Software Model Consistency Checking Tool Based Predicate Logic，ESMCCT），支持对机载嵌入式系统软件的UML模型的类图、顺序图和状态机图之间的自动化一致性检查。最后，通过一个飞机控制机载软件模型的实验，验证了一致性检查工具的实用性。