LusGen: Leveraging LLMs for Safety-Critical Lustre Design and Requirements Traceability
摘要
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.