Cyber-physical systems (CPSs) are complex systems comprised of computational processes, communication networks, and elements interacting with the physical world. The design of the CPSs involves many domain-specific tools and design flows created by engineers with diverse domain knowledge. As the scale of the systems increases, the heterogeneity nature of CPS design prolongs the CPS design process, making exhaustive design-space exploration infeasible. The symbiotic design methodology, in which the designers interact with optimization tools during the design process, is therefore promising to facilitate the design process by performing design exploration in a properly restricted design space. We present a symbiotic design methodology, which explores the design space iteratively and optimizes the system by exploiting the collaboration between designers and tools. The optimization tools perform the design space exploration, while the human designers use their expertise to guide the exploration by restricting the design space. Experimental results based on a robot car configuration problem and an unmanned aerial vehicle design problem show that the methodology can efficiently and effectively discover unconventional designs while optimizing the design objectives.

We present a major new version of Scenic, a probabilistic programming language for writing formal models of the environments of cyber-physical systems. Scenic has been successfully used for the design and analysis of CPS in a variety of domains, but earlier versions are limited to environments that are essentially two-dimensional. In this paper, we extend Scenic with native support for 3D geometry, introducing new syntax that provides expressive ways to describe 3D configurations while preserving the simplicity and readability of the language. We replace Scenic’s simplistic representation of objects as boxes with precise modeling of complex shapes, including a ray tracing-based visibility system that accounts for object occlusion. We also extend the language to support arbitrary temporal requirements expressed in LTL, and build an extensible Scenic parser generated from a formal grammar of the language. Finally, we illustrate the new application domains these features enable with case studies that would have been impossible to accurately model in Scenic 2.