Integrating Reasoning with SysML

Abstract

Abstract Most engineering tasks require in‐depth reasoning. For some tasks, automated reasoning is feasible and can provide high leverage for solving difficult practical problems. Engineering questions can be represented as questions about a model, provided the model contains sufficient domain knowledge. The widely used UML family languages have been embedded within logics. By embedding a model as an axiom set within a suitable logic, engineering questions translate into questions about axiom sets. Automated reasoning can potentially be used to answer these questions. Examples of engineering questions that can be represented as logic questions include verification of a system capability (or a requirement satisfaction) and verification of whether a design change invalidates design constraints. By using this embedding engineers can use languages and tools that they are familiar with, have their models transparently translated into logic, automated inference applied, and the results be returned to their development environment. The logic embedding results of SysML, one of the UML family, is used to illustrate how engineering problems translate into logic problems and how the logic solutions translate back to engineering solutions. An engineering use case for air system capability analysis is used to show how a SysML model can be translated into an axiom set and the engineering question translates into a logic question and illustrates how formal reasoning about an axiom set can be used to answer the engineering question.