Scholarlink

<p>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.</p><p>However, even a&#xa0;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&#xa0;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.</p><p>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.</p><p>Currently a&#xa0;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.</p><p>This paper introduces a&#xa0;multi-step approach that formalizes requirements using Linear Temporal Logic (LTL) and generates operating states and transitions, which are then modeled in a&#xa0;SysML v2 state machine diagram, enhancing both the development process and the system’s reliability.</p>

错误：搜索内容不能为空，请输入英文关键词
错误：关键词超出字数限制，请精简
高级检索

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

  • 期刊论文

  • 出版模式：

    开放获取

  • 发表日期：

    2025年3月14日

查看全文
  • Simon Dehn,
  • Georg Jacobs,
  • Philipp Höck,
  • Gregor Höpfner

摘要

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.