Verifying executability of SysML behavior models using satisfiability modulo theory solvers
Raphaël Barbau, Conrad E. Bock · 2020
This report presents an approach to verifying executability of system behavior models by treating them as logical constraint problems solved using Satisfiability Modulo Theory (SMT).With behavior models interpreted as logical constraints on execution order, these solvers can determine whether the models are executable by finding executions that meet those constraints, or not executable because they are overconstrained.The approach relies on Ontological Behavior Modeling (OBM) to unify behavior modeling in the Systems Modeling Language (SysML) under a logical framework based on its structural elements.Translation patterns are proposed between SysML structural models, OBM, and logical constructs in SMT-LIB, a language used as input to SMT solvers.Software developed based on these patterns automatically translates SysML models extended with OBM into SMT-LIB files.Finally, the approach and software are demonstrated by translating and solving example SysML behavior models.