Enhancing model-based development with formalized requirements: integrating temporal logic and SysML v2 for comprehensive state and transition modeling

Abstract Modern vehicles are complex cyber-physical systems with numerous customer functions and operating states, requiring careful management during development. Ensuring that all potential states and transitions are rigorously defined at the requirement stage is critical for vehicle safety and reliability. Due to stringent regulatory requirements and competitive market pressures, it is essential to articulate these requirements unambiguously, free of redundancy, and correctly. However, even a formally correct set of requirements can be underspecified, leading to unintended operating states that compromise vehicle functionality. To ensure requirement completeness, various approaches have been proposed to generate operating states and transitions allowed by a given set of requirements, ensuring that only intended behaviors are permitted. Existing methodologies often rely on natural language requirements, prone to ambiguities and errors. Furthermore, several methods formalize requirements using temporal logic languages, which can be checked algorithmically. Because of the complexity of modern vehicles, Model Based Systems Engineering (MBSE) has become state of the art in vehicle requirements engineering, as MBSE enables rigorous traceability of requirements and early model-based validation of requirement fulfillment. Currently a gap remains in integrating the comprehensive generation of operating states and transitions with the formalization in temporal logic languages, specifically for the use in MBSE development environments. This paper introduces a multi-step approach that formalizes requirements using Linear Temporal Logic (LTL) and generates operating states and transitions, which are then modeled in a SysML v2 state machine diagram, enhancing both the development process and the system’s reliability.