概率需求下信息物理系统设计的随机假设-保证契约

我们为在概率需求下建模为闭环控制系统的信息物理系统设计，开发了一个假设-保证契约框架。我们使用信号时序逻辑的一种变体，即随机信号时序逻辑（StSTL），来指定系统行为以及契约假设和保证，从而能够对随机系统的需求进行自动推理。给定一个随机线性系统表示和一组由有界StSTL契约捕获的需求，我们提出算法来检查契约的兼容性、一致性和精化，并生成一个控制器以保证契约被满足，遵循随机模型预测控制方法。我们的算法利用将验证和控制综合任务编码为混合整数优化问题，以及概率约束的保守近似，从而产生既可靠又可处理的问题表述。我们通过几个例子展示了我们方法的有效性，包括飞机配电网络嵌入式控制器的设计。