<p>Modern computing infrastructures, including IoT, cloud, and edge environments, require rigorous dependability evaluation to ensure continuous operation despite component failures. Stochastic Petri Nets (SPNs) provide a well-established formalism for modeling failure, repair, and redundancy mechanisms, but constructing correct SPN models can be time-consuming and error-prone. Recent advances in large language models (LLMs) raise the question of whether these systems can assist in constructing formal dependability models. This paper investigates LLMs’ ability to generate SPN availability models for fault-tolerant systems with cold-standby redundancy. Using a structured prompt and a baseline model, six LLM platforms (ChatGPT, Gemini, Claude, DeepSeek, Mistral, and Copilot) were tasked with generating SPN models in Mercury-script notation. The generated models were validated in the Mercury modeling environment and evaluated for lexical and syntactic correctness, semantic fidelity, executability, and agreement with an analytical availability baseline. The results reveal notable differences among the evaluated models. Gemini produced an executable SPN model with minimal adjustments and results consistent with the analytical reference, while ChatGPT, Claude, and Copilot required corrections before execution. In contrast, DeepSeek and Mistral produced models with substantial inconsistencies that prevented execution. These findings suggest that LLMs can accelerate early-stage stochastic dependability modeling but still require expert validation and tool-based verification to ensure correctness.</p>

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

Leveraging large language models for generating availability models of standby structures

  • Paulo Maciel,
  • Dario Vasconcelos,
  • Maria Azevedo,
  • Erick Nascimento,
  • Jamilson Dantas

摘要

Modern computing infrastructures, including IoT, cloud, and edge environments, require rigorous dependability evaluation to ensure continuous operation despite component failures. Stochastic Petri Nets (SPNs) provide a well-established formalism for modeling failure, repair, and redundancy mechanisms, but constructing correct SPN models can be time-consuming and error-prone. Recent advances in large language models (LLMs) raise the question of whether these systems can assist in constructing formal dependability models. This paper investigates LLMs’ ability to generate SPN availability models for fault-tolerant systems with cold-standby redundancy. Using a structured prompt and a baseline model, six LLM platforms (ChatGPT, Gemini, Claude, DeepSeek, Mistral, and Copilot) were tasked with generating SPN models in Mercury-script notation. The generated models were validated in the Mercury modeling environment and evaluated for lexical and syntactic correctness, semantic fidelity, executability, and agreement with an analytical availability baseline. The results reveal notable differences among the evaluated models. Gemini produced an executable SPN model with minimal adjustments and results consistent with the analytical reference, while ChatGPT, Claude, and Copilot required corrections before execution. In contrast, DeepSeek and Mistral produced models with substantial inconsistencies that prevented execution. These findings suggest that LLMs can accelerate early-stage stochastic dependability modeling but still require expert validation and tool-based verification to ensure correctness.