形式化软件规约技术便于软件系统原型、分析、验证与最终的实现，是保证软件质量和提高软件生产率非常有用和重要的手段。但是形式化规约的获取是一项相当困难的任务，因此通过自动化转换获取形式化规约就显得尤为必要，这已经成为需求工程的重要问题之一。在形式化规约的获取任务中，另一个重要问题是形式化规约的正确性，即给定一个问题需求，往往可以获取多种不同形式的形式化规约，如何证明这些不同形式规约正确。　　 本文的研究目标是针对问题需求自动化转换为形式化规约与形式化规约正确性这两个重要问题，一是研究从结构化需求语言SRL到形式化规约语言自动生成系统及其高可靠性理论，二是研究形式化规约的相对正确性问题。为了使研究工作与PAR方法及其支撑平台无缝衔接，本文使用Radl语言作为形式化软件规约语言。　　 围绕研究目标，本文的具体研究内容与成果包括:　　 1.为了减少或消除自然语言固有的歧义性，设计了一种受控自然语言--结构化需求语言(StructuralRequirementLanguage，简称SRL)来描述问题需求。该语言词语、句型、语义和语义都受控，便于普通用户使用。具有功能强大、高度数据抽象和可扩充性、支持泛型机制、丰富的语料库、量词结构化等特点。　　 2.为了描述结构化需求语言SRL与形式化软件规约Radl两个领域不同级别的形式化，并进一步刻画SRL语言与Radl语言之间的转换关系，通过深入分析，提炼出源语言SRL分析规则、目标语言Radl生成规则以及源语言SRL到目标语言Radl转换规则三组规则。使用基于规则的方法，将结构化需求语言SRL通过分析-转换-综合三阶段生成为形式化软件规约Radl。　　 3.在基于规则的生成方法指导下，设计并实现了结构化需求语言SRL到形式化软件规约Radl的生成系统SRLtoRadl。使用自然语言处理(NaturalLanguageProcessing，简称NLP)的技术对生成系统SRLtoRadl词法分析、语法分析、语义分析中的诸多难点进行了处理。　　 4.利用范畴论的基本概念:范畴、和（积）、外推（回拉）、余极限（极限）、函子（反变函子）、遗忘函子等，使用范畴论框架逐步的建立了SRLtoRadl生成系统生成过程的语义模型，它是SRLtoRadl生成系统高可靠性的理论基础。　　 5.提出一种基于形式化推导的方法来验证与确认同一问题不同形式规约，这是通过证明不同形式规约与问题需求某个最为直截明了的形式化规约Si等价来达到的，而Si使用PAR方法和PAR平台转换为可执行程序，通过测试已经得到确认。为了支持该方法，进一步提出了扩展的逻辑系统和辅助证明算法。