Stochastic contracts for cyber-physical system design under probabilistic requirements
Stochastic contracts for cyber-physical system design under probabilistic requirements
复制标题
概率要求下的网络物理系统设计的随机契约
DOI：
10.1145/3127041.3127045
复制
发表时间：
2017
期刊：
影响因子：
--
通讯作者：
Dewei Li
中科院分区：
文献类型：
--
作者：
Jiwei Li;P. Nuzzo;A. Sangiovanni;Y. Xi;Dewei Li
我们开发了一个假设保证合同框架的网络物理系统的设计，建模为闭环控制系统，概率要求。我们使用一个变种的信号时序逻辑，即随机信号时序逻辑（StSTL）指定系统的行为以及合同的假设和保证，从而使自动推理的随机系统的要求。给定一个随机线性系统表示和一组有界StSTL合同捕获的要求，我们提出了算法，可以检查合同的兼容性，一致性和细化，并生成一个控制器，以保证合同得到满足，随机模型预测控制方法。我们的算法利用混合整数优化问题的验证和控制合成任务的编码，以及产生声音和易于处理的问题配方的概率约束的保守近似。我们说明了我们的方法的有效性，在几个例子，包括飞机配电网络的嵌入式控制器的设计。
We develop an assume-guarantee contract framework for the design of cyber-physical systems, modeled as closed-loop control systems, under probabilistic requirements. We use a variant of signal temporal logic, namely, Stochastic Signal Temporal Logic (StSTL) to specify system behaviors as well as contract assumptions and guarantees, thus enabling automatic reasoning about requirements of stochastic systems. Given a stochastic linear system representation and a set of requirements captured by bounded StSTL contracts, we propose algorithms that can check contract compatibility, consistency, and refinement, and generate a controller to guarantee that a contract is satisfied, following a stochastic model predictive control approach. Our algorithms leverage encodings of the verification and control synthesis tasks into mixed integer optimization problems, and conservative approximations of probabilistic constraints that produce both sound and tractable problem formulations. We illustrate the effectiveness of our approach on a few examples, including the design of embedded controllers for aircraft power distribution networks.