Safety-critical systems require precise software modeling and requirements traceability, with Lustre widely used for formal design. Large language models (LLMs) struggle with Lustre’s syntax and semantics. We propose LusGen, the first LLM-based Lustre generation approach that integrates domain knowledge via prompt engineering and retrieval-augmented generation, combined with syntax checking and semantic verification feedback for iterative refinement. LusGen also enables fine-grained requirements-to-design traceability compliant with DO-178C. We conduct an empirical study revealing hallucination patterns in Lustre generation to guide our approach. Evaluations on four datasets show that LusGen improves syntax correctness to 98%, semantic correctness to 94%, and achieves over 88% accuracy in traceability, demonstrating practical industrial applicability. We also construct a benchmark dataset to advance future research.

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

LusGen: Leveraging LLMs for Safety-Critical Lustre Design and Requirements Traceability

  • Yili Jiang,
  • Zhuoran Yan,
  • Ning Ge,
  • Yuan Wang,
  • Jiahao Weng,
  • Chunming Hu

摘要

Safety-critical systems require precise software modeling and requirements traceability, with Lustre widely used for formal design. Large language models (LLMs) struggle with Lustre’s syntax and semantics. We propose LusGen, the first LLM-based Lustre generation approach that integrates domain knowledge via prompt engineering and retrieval-augmented generation, combined with syntax checking and semantic verification feedback for iterative refinement. LusGen also enables fine-grained requirements-to-design traceability compliant with DO-178C. We conduct an empirical study revealing hallucination patterns in Lustre generation to guide our approach. Evaluations on four datasets show that LusGen improves syntax correctness to 98%, semantic correctness to 94%, and achieves over 88% accuracy in traceability, demonstrating practical industrial applicability. We also construct a benchmark dataset to advance future research.