Design Automation for Smart Factories

The paper titled Quantitative Verification and Design Space Exploration Under Uncertainty with Parametric Stochastic Contracts, authored by Chanwook Oh, Michele Lora and Pierluigi Nuzzo, has been accepted at the 2022 IEEE International Conference on Computer-aided Design (ICCAD)

This paper proposes an automated framework for quantitative verification and design space exploration of cyber-physical systems in the presence of uncertainty, leveraging assume-guarantee con- tracts expressed in Stochastic Signal Temporal Logic (StSTL). We introduce quantitative semantics for StSTL and formulations of the quantitative verification and design space exploration problems as bi-level optimization problems. We show that these optimization problems can be effectively solved for a class of stochastic systems and a fragment of bounded-time StSTL formulas. Our algorithm searches for partitions of the upper-level design space such that the solutions of the lower-level problems satisfy the upper-level constraints. A set of optimal parameter values are then selected within these partitions. We illustrate the effectiveness of our framework on the design of a multi-sensor perception system and an automatic cruise control system.