摘要：形式化软件规约技术是保证软件质量和提高软件生产率非常有用和重要的手段，但是形式化软件规约的获取是需求工程中一项相当困难的任务．本文针对问题需求自动化转换为形式化规约这个重要问题，研究从结构化需求语言SRL到形式化规约语言Radl自动生成系统及其高可靠性理论．为此，设计了一种受控自然语言．结构化需求语言SRL来描述问题需求；使用基于规则的方法，将结构化需求语言SRL通过分析．转换一综合三阶段生成为形式化软件规约Radl；在该方法的指导下，设计并实现了从结构化需求语言SRL到形式化软件规约Radl的生成系统SRLtoRadl；进一步，使用范畴论框架建立了SRLtoRadl生成系统生成过程的语义模型．实际效果表明该系统能有效的生成高质量形式化软件规约Radl．

关键词：结构化需求语言 形式化软件规约 自动生成系统 高可靠 范畴论语义 

单位：江西师范大学省高性能计算技术重点实验室; 江西南昌330022; 中国科学院软件研究所计算机科学国家重点实验室; 北京100190; 中国科学院研究生院; 北京100190; 江西师范大学计算机信息工程学院; 江西南昌330022