保持行为程序存活：指定与执行活性需求

使用可执行规范（如行为编程，Behavioral Programming）的一个好处是能够将系统实现与其需求保持一致。这在 BP 通过一种协议实现，其中允许独立实现的模块指定系统可能、必须或不得不做的事。通过这种方式，每个模块都可以强制执行单个系统需求，包括负向规范，如“在 Y 之后不要做 X”。然而，现有的 BP 协议仅允许执行安全需求，不支持诸如“至少做三次 X”之类的活性属性的执行。为在 BP 中直接和独立地建模活性需求，我们提出了一种为状态标记“must-finish”（必须完成）的习惯用法，以指示尚未完成的任务。我们展示，这种习惯用法允许直接指定文献中已知的需求模式。我们还提供了语义和两种执行机制：一种基于将其翻译为 Büchi 自动机，另一种基于马尔可夫决策过程（MDP）。后者方法的潜在优势在于能够有效地处理大型软件系统。本文通过一个概念验证工具，对提出的方法进行定性和定量评估。对 MDP 基于的执行机制进行了形式化分析，附录中给出。