Formal methods for a system of systems analysis framework applied to traffic management

Formal methods for systems and system of systems engineering (SoSE) can bring precision to architecting and design, and increased trustworthiness in verification; but they require the use of formal languages that are not broadly comprehensible to the various stakeholders. The evolution of Model Based Systems Engineering (MBSE) using the Systems Modeling Language (SysML) lies in a middle ground between legacy document-based SoSE and formal methods. SysML is a graphical language but not a formal language. Initiatives in the Object Management Group (OMG), such as the development of the Foundational Unified Modeling Language (fUML) seek to bring precise semantics to object-oriented modeling languages. Following the philosophy of fUML, we offer a framework for associating precise semantics with Unified Modeling Language (UML) and SysML models essential for SoSE architecting and design. Straightforward methods are prescribed to develop the essential models and to create semantic transformations between them. Matrix representations can be used to perform analyses that are concordant with the system of UML or SysML models that represent the system or SoS. The framework and methods developed in this paper are applied to a Traffic Management system of systems (TMSoS) that has been a subject of research presented at previous IEEE SoSE conferences.