Safe Alone, Dangerous Together

Modern safety-critical systems — autonomous vehicles, surgical robots, smart power grids — are built by composing independently developed cyber-physical components: perception modules, planning algorithms, control systems, actuators, and communication networks. Each component may be individually verified against its specification, but when composed into a complete system, emergent behaviors arise that violate safety properties none of the individual component tests would reveal. An individually verified perception module and an individually verified planner can, when connected, produce unsafe trajectories because their assumptions about timing, uncertainty representation, and failure modes are subtly incompatible. No compositional verification framework exists that can guarantee system-level safety from component-level proofs for cyber-physical systems where physical dynamics couple component behaviors.

The aerospace and automotive industries are shifting toward modular, component-based development to reduce costs and enable innovation. SAE's FACE (Future Airborne Capability Environment) standard for military avionics and AUTOSAR for automotive software both envision plug-and-play safety-critical components. However, the FAA, NHTSA, and DoD cannot certify systems built this way without compositional safety arguments, creating a bottleneck where the development model outpaces the certification framework. The cost of full-system verification grows exponentially with system size, making monolithic verification impractical for complex systems-of-systems. Without compositional verification, every integration change requires re-verifying the entire system — negating the modularity benefits.

Assume-guarantee reasoning — the standard compositional verification approach in software — assumes that components interact only through well-defined interfaces with discrete, logical specifications. CPS components interact through continuous physical dynamics (forces, electromagnetic fields, thermal coupling) that cannot be fully captured in discrete interface contracts. Contract-based design (using tools like OCRA, Pacti) can compose system guarantees from component contracts but requires that contracts be expressible in the same formal language, which is difficult when components span discrete (software), continuous (control), and stochastic (ML) domains. Model-based systems engineering (MBSE) tools (SysML, Simulink) support integrated simulation but not formal verification of composed systems. Runtime assurance approaches (simplex architecture) can monitor for safety violations and switch to verified backup behaviors, but this sacrifices the performance of the primary system and doesn't address the root composability problem.

A contract language expressive enough to capture the continuous-time, hybrid (mixed continuous-discrete), and stochastic behaviors of CPS components, with composition operators that compute system-level guarantees from component contracts. Practical algorithms for contract verification that scale to realistic component sizes. Standardized testing protocols that systematically probe component interactions at interface boundaries — the "seams" where composed systems fail — rather than testing components in isolation.

A student team could take a simple composed CPS (e.g., a drone with separate perception, planning, and control modules) and demonstrate specific safety violations that arise from composition but don't appear in individual component testing, documenting the failure patterns and interface assumption mismatches. Alternatively, a team could implement contract-based composition for a two-component CPS (e.g., adaptive cruise control with separate sensor and controller) using an existing contract framework (Pacti), measuring the gap between composed guarantees and empirically observed behavior. Relevant disciplines include systems engineering, control theory, formal methods, and embedded systems.