Skip to main content
U.S. flag

An official website of the United States government

Official websites use .gov
A .gov website belongs to an official government organization in the United States.

Secure .gov websites use HTTPS
A lock ( ) or https:// means you’ve safely connected to the .gov website. Share sensitive information only on official, secure websites.

Verifying executability of SysML behavior models using Satisfiability Modulo Theory solvers



Raphael Barbau, Conrad E. Bock


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.
NIST Interagency/Internal Report (NISTIR) - 8283
Report Number


SysML, behavior verification, systems modeling


Barbau, R. and Bock, C. (2020), Verifying executability of SysML behavior models using Satisfiability Modulo Theory solvers, NIST Interagency/Internal Report (NISTIR), National Institute of Standards and Technology, Gaithersburg, MD, [online], (Accessed June 17, 2024)


If you have any questions about this publication or are having problems accessing it, please contact

Created February 14, 2020, Updated June 18, 2020