J. Smith
Imandra, Texas, United States
Keywords: LLM, Gen AI, SysML, MBSE, Formal Methods
Digital engineering is critical to staying ahead of the technology curve and ensuring global competitiveness for our warfighters. SysML (Systems Modeling Language) is a widely-used formalism and international standard for designing and communicating complex system designs, and is especially relied upon in the development of safety-critical autonomous systems. SysML v2 is a major new version of SysML. SysML v2 introduces a formal semantics for specifying the precise meaning of SysML models, which makes it possible to apply formal verification and automated reasoning to analyze safety and correctness properties of SysML designs automatically. The introduction of LLMs allows engineers to use natural language to analyze and extend their models. During this talk, we will demonstrate our research and what we have learned using Automated Reasoning with SysML v2 models to: - Mathematically prove properties of system correctness. - Formal models checking of state machines and other behavior models - Add a hallucination-free natural-language interface (chatbot) to empower more stakeholders to gain insights and leverage the SysML v2 model. - Formal impact analysis of changes in the model - Automated proofs that requirements are met by the model