Compositional Reasoning over System Architectures with Integrated Cognitive Models

Model-based systems engineering (MBSE) for cyber–physical systems increasingly must account for human operators who work with the growing autonomy. For safety- and security-critical applications, it is not sufficient to verify the cyber–physical platform in isolation; the system architecture must also capture assumptions about human cognition and provide evidence that operators are not put at risk. This paper presents a methodology for architecture-centric modeling and compositional verification that couples a system model with an executable cognitive model of the operator. System structure and contracts are described in the Architecture Analysis and Design Language (AADL) with AGREE assume–guarantee specifications, while operator behavior is encoded in a Soar-based cognitive model. AADL serves as the MBSE backbone, enabling engineers to represent hardware, software, communication, and human-in-the-loop components in a single, analyzable architectural model. An automated translation pipeline builds a unified model for model checking in nuXmv, enabling verification of temporal-logic properties that relate system architecture to safety of the human operator (e.g., avoidance of cybersickness, safe sensor handover). We illustrate the approach in realistic mixed-reality and increasingly autonomous system case studies, showing how architectural decisions, cognitive assumptions, and formal-methods tooling can be combined to support end-to-end assurance arguments in safety- and security-critical deployment contexts.