The industry is undergoing a significant digital transformation in the way system requirements are defined, communicated, and managed. Major original equipment manufacturers (OEMs) are moving toward fully model-based development processes, with plans to deliver requirements exclusively in the form of system models. It is no longer sufficient to manage requirements using traditional document-based approaches; instead, organizations must adopt tools and processes that enable the consumption, interpretation, and implementation of model-based requirements. Preparing to meet this industry direction is critical to maintaining competitiveness and alignment with our customers’ expectations.
Model-Based Systems Engineering (MBSE) plays a central role in this transition. MBSE enables engineers to define, analyze, and manage system requirements, architectures, behaviors, and verification strategies within a cohesive model-based framework. It supports traceability, promotes consistency across views, and improves collaboration across multidisciplinary teams. However, MBSE by itself does not ensure that the requirements defined within the model are correct, complete, or consistent. Without rigorous validation techniques, even well-structured models can carry forward poorly defined or conflicting requirements—leading to errors that propagate throughout the development lifecycle.
Several analyses have shown that requirement-related issues are a leading cause of program delays and cost overruns. Surveys indicate that over 50% of issues discovered at the Entry into Service (EIS) stage can be traced back to ambiguous, incomplete, or inconsistent requirements. These types of defects are often not detected until the verification and validation phases, at which point their correction becomes significantly more costly and time-consuming. Industry estimates suggest that requirement defects discovered late in the lifecycle can be up to 20 times more expensive to fix compared to those caught early during requirements engineering.
Given the increasing complexity of systems, which may include thousands of interdependent requirements across mechanical, electrical, and software domains, it is no longer practical to rely solely on manual inspection or peer reviews to detect these issues. This challenge calls for a more formalized and automated approach—one that combines the structural rigor of MBSE with the analytical precision of formal methods.
Formal methods offer mathematically rigorous techniques to verify the properties of system requirements and designs. They allow engineers to check for logical consistency, completeness, and conformance to standards, thereby reducing ambiguity and improving
This document does not contain any Export Controlled Technical Data
the quality of the engineering artifacts. However, the current ecosystem of MBSE tools lacks robust native support for such analyses. For example, Cameo Systems Modeler—a widely adopted SysML modeling tool used by various organizations—does not currently provide built-in capabilities for formally analyzing requirement completeness or consistency. This limitation represents both a risk and a strategic opportunity.
This work proposes an approach that integrates formal methods into MBSE workflows by enabling completeness and consistency checks of SysML-based requirements within Cameo. The method bridges Cameo with formal analysis tool by transforming formalized requirements in Cameo into analyzable models. The transformation enables formal verification and automated test generation, allowing engineers to identify missing, conflicting, or unreachable requirements early in the development lifecycle.
The proposed methodology begins with formalizing system requirements in SysML using a structured modeling approach. Most functional requirements are captured using activity diagrams or sequence diagrams, while performance and constraint requirements are formalized using parametric diagrams. These models are then transformed into equivalent representations in formal analysis tool where they can be analyzed. The transformation process preserves traceability to the original requirements in Cameo, ensuring alignment between the system model and the verification artifacts.
The formal analysis tool is used to perform completeness and consistency checks, such as identifying unreachable logic, missing input cases, or contradictory requirement conditions. The tool can also automatically generate test cases that demonstrate coverage of the formalized requirements. These test cases serve a dual purpose: they provide early validation of the system behavior and can be reused during design verification activities.
This approach offers multiple benefits. First, it supports compliance with industry standards which mandate that aircraft and system-level requirements must be complete and correct. Second, it reduces reliance on manual inspection, enabling more scalable and automated requirement validation. Third, it introduces a new capability that fills a critical gap in existing MBSE tooling.
In conclusion, as the industry transitions to delivering and consuming model-based requirements, the integration of formal methods into MBSE is essential for ensuring quality and reducing development risk. This work represents a foundational step in building an MBSE ecosystem that is not only descriptive but also analytically robust. By combining the expressive power of SysML with the validation strength of formal analysis tools.