Automating Physics-Based Reasoning for SysML Model Validation
Candice Chambers, Summer Mueller, Parth Ganeriwala, Chiradeep Sen, Siddhartha Bhattacharyya
TL;DR
The paper addresses the gap in SysML MBSE validation by introducing an automated physics-based reasoner that enforces physical laws on both structural (BDD/IBD) and functional (Activity) diagrams. It combines a formal function representation with physics-based verification, organized into three inspections—Balance Laws, Incomplete Topology, and Inferred Balance—and supported by a functional knowledge base. The framework is implemented through modules that extract model knowledge and apply the inspections, and it is validated on four electromechanical use cases (coffeemaker, hair dryer, vacuum cleaner, wired speaker), revealing inconsistencies detectable only through physics-based reasoning. The work demonstrates improved early verification of physical validity in SysML models and outlines future expansions of the KB and integration with English-specification pipelines to broaden applicability and automation in practice.
Abstract
System and software design benefits greatly from formal modeling, allowing for automated analysis and verification early in the design phase. Current methods excel at checking information flow and component interactions, ensuring consistency, and identifying dependencies within Systems Modeling Language (SysML) models. However, these approaches often lack the capability to perform physics-based reasoning about a system's behavior represented in SysML models, particularly in the electromechanical domain. This significant gap critically hinders the ability to automatically and effectively verify the correctness and consistency of the model's behavior against well-established underlying physical principles. Therefore, this paper presents an approach that leverages existing research on function representation, including formal languages, graphical representations, and reasoning algorithms, and integrates them with physics-based verification techniques. Four case studies (coffeemaker, vacuum cleaner, hairdryer, and wired speaker) are inspected to illustrate the model's practicality and effectiveness in performing physics-based reasoning on systems modeled in SysML. This automated physics-based reasoning is broken into two main categories: (i) structural, which is performed on BDD and IBD, and (ii) functional, which is then performed on activity diagrams. This work advances the field of automated reasoning by providing a framework for verifying structural and functional correctness and consistency with physical laws within SysML models.