  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.
