A Semantics Modeling Approach Supporting Property Verification based on Satisfiability Modulo Theories

Property verification in Model-based systems engineering (MBSE) supports the formalization of model properties and evaluates the constraints of model properties to select an optimal system architecture from alternatives for tradeoff optimization. However, there is a lack of an integrated method that property verification enables to be applied in multi domain specific modeling languages, which is not conductive to the reuse of property verification for different architecture and may increase the learning and use cost. To solve the problem, a semantic approach combining a unified modeling method GOPPRRE modeling method with Satisfiability Modulo Theories (SMT) is proposed to realize property verification. The syntax of the multi-architecture modeling language KARMA based on the GOPPRRE modeling method is extended to realize property verification based on Satisfiability Modulo Theories, which enables the KARMA language to verify the models by evaluating the constraints which are defined based on the model properties. The proposed approach supports the evaluation of property constraints defined by different modeling languages for trade-off optimization in a unified language. The approach is evaluated by a case of optimizing the matching between workers and processes in a multi-architecture modeling tool MetaGraph which is developed based on KARMA. From the result, such approach enables to evaluate constraints consisting of properties and select an optimal scheme from the alternatives.