Skip to main content
U.S. flag

An official website of the United States government

Dot gov

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

Https

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

Published

Author(s)

Raphael Barbau, Conrad E. Bock

Abstract

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

Keywords

SysML, behavior verification, systems modeling
Created February 14, 2020, Updated June 18, 2020