Engineering systems that involve physical elements controlled by computational infrastructure are called Cyber-Physical Systems (CPS). CPS are present in almost every modern automated system, ranging from manufacturing and transportation systems over telecommunication networks to large-scale computer clusters. The ever-increasing demand for safety, security, performance, and certification of these — often safety-critical — CPS put stringent constraints on their design. This necessitates the use of formal, model-based approaches to analyze and design secure, reliable and performant systems.

In the past decades, formal, model-based approaches to control software synthesis for CPS have gained more and more attention both in the Control Engineering and in the Computer Science Community. While these approaches are applicable to the entire control stack, this workshop focuses mostly on the top layer of the control hierarchy. Here, supervisory control and coordination software orchestrates the interplay of different system components and needs to ensure their safe and reliable behavior.

The main objective of this workshop is to bring researches from control and computer science together to discus recent results and open problems in this research area.

In particular, this workshop will focus on two specific recent topics in the verification and synthesis of CPS:

Topic A: Structural Properties in Controller Synthesis

Scalability is one of the major challenges when applying formal methodologies to large-scale CPS due to the extremely large state-space. One way to address the inherent difficulty in analyzing or controlling complex, large-scale, interconnected systems, is to apply a “divide and conquer” strategy, namely, compositional approaches.
Such approaches, in general, leverage the structural properties of CPS by taking well-defined sub-system interactions into account. In addition, a high degree of decentralization is only achieved if control software is permissive — i.e., allows for local adaptations and specializations, especially when humans are in the feedback loop. In past years, many structural properties such as compositionality and permissiveness have been investigated extensively by different researchers from different angles.
This workshop aims to gather recently developed novel approaches for synthesis of CPS leveraging structural properties.

Topic B: Information-Flow Properties in Dynamic Systems

In correct-by-construction synthesis of safety-critical CPS, existing works mainly focus on the correctness of the internal behavior of the system. However, in many practical scenarios, CPS are usually partially-observed — either from the system-user’s point of view due to the limited sensing capabilities, or from the outsider’s point of view due to the partial information release.
In this case, the design objective can also be related to the information-flow of the dynamic systems. In the control community, researchers have investigated many different notions of information-flow properties such as diagnosability, observability, detectability and opacity.
Recently, a new temporal logic in the computer science literature called HyperLTL has been studied very actively, which has been shown as a very suitable tool for expressing information-flow properties.
This workshop also aims to discuss the recent developments in correct-by-construction synthesis of CPS for information-flow properties, which is the key in ensuring security for CPS.