Scaling CPS Understanding

The intricate interplay of software, hardware, and multi-physics in large-scale cyber-physical systems (CPS) exceeds the cognitive capacity of even the most experienced engineers. Although standards such as SysML 2.0 improve how systems are organized structurally, they lack the deep semantic foundation necessary to prevent misunderstandings and late-stage failures. We propose a rigorous, logic-based framework that enhances comprehension by breaking down complex CPS causal chains and by converting implicit design assumptions into explicit, testable behavioral models.

Stream calculus addresses the complexity collapse by modeling CPS as networks of components that interact through timed or untimed data streams. Defining each system element as a mathematical function that maps input histories to output histories eliminates semantic ambiguity and provides a rigorous formalization of intertwined discrete and continuous behaviors. This semantic grounding turns CPS design into a proactive discipline. It enables engineers to master compositionality and resilience by using purposeful abstractions and causal analysis instead of reactive failure analysis. The technical foundation of stream calculus relies on:
• Interface specifications to encapsulate the behavior of input and output streams, accommodating intertwined discrete-time and dense-time streams.
• Strong causality and realizability to facilitate a dual denotational and operational understanding, grounding the functional behavior of specifications in the state-based logic of extended Moore machines.
• Concurrent composition of mutually interacting interface specifications to support modular reasoning. The construction of unique fixed points for strongly causal stream transformers is novel and relies on the Baire metric on streams. A sound and relatively complete calculus manages interactions, and ensures that the behavior of the whole is predictable based on that of its parts.
• Refinement to formally reduce under-specification and to ensure that concrete realizations remain logically consistent with their abstract origins. This supports a comprehensive understanding of the system by verifying that each layer of refinement remains consistent with the abstract behavioral model.
• Multi-viewpoint architectures to enhance CPS understanding by partitioning cross-domain complexity into cognitively manageable perspectives, such as functional, logical, and physical views, which are tailored to specific engineering concerns. The framework enforces semantic consistency between these viewpoints to prevent mental fragmentation, providing a unified model in which the causal interactions between software control and physical behavior remain transparent and predictable. 

The Software Platform Embedded Systems (SPES) projects conclude that mastering the complexity of modern CPS requires transitioning from informal structural diagrams to a rigorous, model-based engineering framework. Central to this conclusion is the use of stream calculus in industrial automotive, aerospace, and medical use cases as a formal semantic foundation that eliminates ambiguity and supports modular development.

In summary, the main benefit of using stream calculus in CPS design is replacing ambiguous natural language documentation with semantically consistent models. It effectively converts implicit design dependencies into explicit, verifiable architectures. Engineers can then examine the causal logic of complex behaviors through rigorous causal and counterfactual analyses based on formal evidence. Consequently, this methodology ensures that emergent risks and critical edge cases are identified and mitigated before implementation details obscure the underlying system logic.

Relevance to HCSS 2026: This semantically grounded design calculus provides the necessary foundation for principled digital engineering, particularly in closing the MOSA (Modular Open Systems Approach) assurance gap. The framework offers formal protection against complexity collapse by encapsulating untrusted supply chain components within strict interface specifications. This rigorous encapsulation ensures the system’s behavioral integrity remains intact when integrating opaque or unverified third-party elements. Ultimately, this approach moves beyond reactive failure analysis, establishing a unified model where the causal interactions between software control and physical behavior remain transparent, predictable, and verifiable.
 

Harald Ruess is a principal scientist at SRI, where he directs the Formal Methods and Dependable Systems program. He has made significant contributions to several widely used specification and verification tools, including PVS, SAL, and ETB. In 2021, Harald received the CAV Award for his pioneering role in developing SMT and its applications. Harald was the scientific and managing director of FORTISS, the Bavarian research institute for software and systems engineering associated with the Technical University of Munich. He also has extensive experience as a systems engineering consultant for the automotive and aerospace industries.