The aerospace industry is undergoing a significant digital transformation in the way system requirements are defined, communicated, and managed. Major OEMs are moving towards fully model-based development processes, with plans to deliver requirements exclusively in the form of 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.
However, MBSE itself does not ensure that the requirements defined within the model are 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.
This work proposes an approach that integrates formal methods into MBSE workflows by enabling completeness and consistency checks of SysML-based requirements within Cameo Systems Modeler. The method bridges Cameo Systems Modeler with formal analysis tool by transforming modeled requirements in Cameo into analyzable formal specification. The transformed formal requirements allow engineers to identify missing, conflicting, or unreachable requirements early in the development lifecycle, while also aiding automated test generation.