利用行为工程数学框架检测需求缺陷

行为工程（Behavior Engineering, BE）提供了一种严格的方法，能够从自然语言编写的需求中导出软件系统的形式化规约。其图形化规约语言行为树（Behavior Tree, BT）已在工业界成功应用，用于将大型、复杂且常常存在错误的需求系统地转化为软件系统的集成模型。BE 的流程，即行为建模流程（Behavior Modeling Process, BMP），允许将需求逐一翻译为单个需求 BT，随后将它们集成以形成系统的整体视图。集成的 BT 随后经历一系列修改以构建用于确认和验证的规约 BT。BMP 还在其整个流程中处理需求中的不同类型的缺陷。然而，BT 本身是一种图形化建模表示法，集成关系的类型、它们如何对应特定问题、应如何集成以及如何获得形式化规约尚未被清晰定义。因此，BMP 是非形式化的，仅提供以临时方式执行所有这些任务的指南。在本文中，我们首先引入一个数学框架来定义 BT 的图形形式，我们利用它来定义 BT 的集成关系并形式化 BMP 的集成策略。然后，我们利用这一底层数学框架制定了半自动化的需求缺陷检测技术，该框架可扩展用于形式化 BMP、为其开发变更管理框架、构建往返工程技术等。