digital · infrastructure · family: the answer is in a field you’ve never heard of
safealone,dangeroustogether
Verified cyber-physical system components lose safety guarantees when composed
Problem statement
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.
Why this matters
The aerospace and automotive industries are shifting toward modular, component-based development to reduce costs and enable innovation. The 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.
What’s been tried and why it hasn’t worked
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.
What would unlock progress
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.
Entry points for student teams
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.
Genes
Structural cousins: stuck the same way, in other fields
Sources
NSF CISE CPS Foundations and Connected Communities Program (NSF 25-543); NSF SHF Program; CMU SEI research on Certifiable Distributed Runtime Assurance; accessed 2026-02-15 go to source ↗
Working notes
Notes made while writing and checking this brief, shown as written. They use working shorthand.
The earlier NSF CPS solicitation (NSF 24-581, now archived and replaced by NSF 25-543) said the CPS program "aims to develop the core research needed to engineer these complex CPS, some of which may also require dependable, high-confidence, or provable behaviors." It said the program "seeks to reveal cross-cutting, fundamental scientific and engineering principles that underpin the integration of cyber and physical elements across all application domains." CMU SEI's research on Certifiable Distributed Runtime Assurance (CDRA) specifically addresses component-level safety monitoring as a stepping stone toward compositional certification. Related problems: autonomous-systems-formal-verification.md addresses formal verification of individual autonomous systems; digital-ml-component-formal-verification.md addresses the ML-specific verification barrier; this brief addresses the composition problem when individually verified components are assembled into systems.
Reconciliation 2026-09-29: Fact repair after a site review read this write-up against its sources. The NSF program page in the Source line was fetched in full on 2026-09-29 from https://www.nsf.gov/funding/opportunities/cps-cyber-physical-system-foundations-connected-communities. The page gives the program name as "Cyber-Physical System Foundations and Connected Communities (CPS)" and the solicitation as NSF 25-543, which matches the Source line. The page says it was last updated on August 18, 2025. (1) The two quotations in the paragraph above were given as the words of the NSF CPS program, but they are not on the cited page and not in the NSF 25-543 solicitation. Both are in the earlier solicitation, "NSF 24-581: Cyber-Physical Systems (CPS)", read on 2026-09-29 at https://www.nsf.gov/funding/opportunities/cps-cyberphysical-systems/503286/nsf24-581/solicitation. That page is marked as archived and replaced by NSF 25-543. The paragraph now names NSF 24-581 as where the quotations come from. The first quotation also left out one word; the solicitation says "these complex CPS", and the word has been put back. (2) The text said "SAE's FACE". The Open Group's page for the standard (https://www.opengroup.org/face, fetched 2026-09-29) says the FACE Technical Standard was developed by The Open Group FACE Consortium, and it does not mention SAE. The name "SAE's" was removed. Confirmed and left as written: formal methods for verification and assurance of cyber-physical systems are an area of interest on the NSF CPS page; the NSF Software and Hardware Foundations page (https://www.nsf.gov/funding/opportunities/shf-software-hardware-foundations) lists compositionality and compositional methods for systems with discrete and continuous behavior; the SEI library entry "Certifiable Distributed Runtime Assurance" by Dionisio de Niz, dated October 23, 2018 (https://www.sei.cmu.edu/library/certifiable-distributed-runtime-assurance-2/) describes enforcers that monitor components and the checking that enforcers on several nodes implement a global safety policy; a 2017 SEI paper by Chaki and de Niz, "Certifiable Runtime Assurance of Distributed Real-Time Systems", says the Simplex architecture switches from an efficient untrusted controller to a trusted inefficient one, uses assume-guarantee reasoning, and calls the composition of timing and logical contracts an open challenge; Pacti is a public, open-source package (https://github.com/pacti-org/pacti). NOT checked, because none of the pages read states them and the Source line gives no address for them: that no compositional verification framework exists for cyber-physical systems; that the FAA, NHTSA and DoD cannot certify modular systems without compositional safety arguments; that the cost of full-system verification grows exponentially with system size; the descriptions of AUTOSAR, OCRA, SysML and Simulink; and the example of a perception module and a planner producing unsafe trajectories. These are left as written. Genes untouched.