一句话：提出一个结合 UML 建模、LLM 辅助与演绎验证的需求工程框架，可自动生成程序骨架。
需求工程对软件质量至关重要，但将建模、LLM 与形式验证整合仍具挑战。本文提出一个面向需求工程的综合框架，聚焦特定 UML 图以支持初步系统开发。框架在各建模阶段提供可视化，并无缝集成大语言模型与逻辑推理引擎：由 LLM 辅助生成的行为模型可自动转换为形式逻辑规约，再通过演绎形式验证检查逻辑需求及软件制品间关系是否被充分处理。最终，框架支持自动生成程序骨架，简化从设计到实现的过渡。摘要未报告实验评估，贡献主要在框架设计与流程集成。
The requirements engineering (RE) phase is pivotal in developing high-quality software. Integrating advanced modelling techniques with large language models (LLMs) and formal verification in a logical style can significantly enhance this process. We propose a comprehensive framework that focuses on specific Unified Modelling Language (UML) diagrams for preliminary system development. This framework offers visualisations at various modelling stages and seamlessly integrates large language models and logical reasoning engines. The behavioural models generated with the assistance of LLMs are automatically translated into formal logical specifications. Deductive formal verification ensures that logical requirements and interrelations between software artefacts are thoroughly addressed. Ultimately, the framework facilitates the automatic generation of program skeletons, streamlining the transition from design to implementation.