Automating Physics-Based Reasoning for SysML Model Validation

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.