Verifying executability of SysML behavior models using Satisfiability Modulo Theory solvers

Published

February 14, 2020

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

NIST Pub Series

NIST Interagency/Internal Report (NISTIR)

Pub Type

NIST Pubs

Download Paper

https://doi.org/10.6028/NIST.IR.8283

Local Download

Keywords

SysML, behavior verification, systems modeling

Citation

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], https://doi.org/10.6028/NIST.IR.8283 (Accessed April 19, 2024)