NIST Researchers Explain Software that Finds Inconsistencies in System Behavior Design

NIST’s Raphael Barbau and Conrad Bock were invited to present NIST-developed software that helps find inconsistencies in system behavior designs, at the University of Maryland’s Frontiers in Design Representation Summer School. The week-long event focused on emerging mathematical, statistical, and computing foundations to aid engineering design.

The NIST software Automated translator from OBM to SMT is intended for use with the Systems Modeling Language (SysML), a widely used standard for specifying requirements, design and testing of complex systems.  The software leverages a technique Bock developed in previous work on SysML,  Ontological Behavior Modeling (OBM), which gave a mathematical foundation on which to express system behavior.  Barbau’s software converts system behaviors on this foundation into a widely used file format for stating logical problems in Satisfiability Modulo Theory (SMT), a more general form of Boolean Satisfiability (SAT).

Once engineers have applied NIST’s SysML-based approach to design a complex system, they can use the NIST software to automatically detect inconsistencies in how system behavior is specified. The software converts the SysML models into a logical problem, and then uses an open-source logical solver to find inconsistencies using automated reasoning, so that engineers can rectify the system’s design.