形式化软件规约Radl获取、验证与确认方法研究

Based on our long-term work of (semi)automatic development from the foraml software spefication-Radl to executable program. Further,the project study in-depth how to acquire, verify and validate the formal spcifation Radl, which are two important problems in current software engineering automation and requirement engineering. 1. To acquire Radl specifiation, design a controlled natural language-SRL to describe the problem requirement，then convert SRL into Radl using rule-based method. Combine with the natural language processing technology to seek solutions to many difficulties in the process of convertion. Thus, design and implement a generation system-SRLtoRadl from SRL to Radl. Furthermore, explore to establish the trustworthy semantic model of the generation system using category theory framework. 2. ?Propose a formal derivation method to verify and validate different form specifications of the same problem requirement. The basic idea is proving the equivalency between different forms of Radl specifications and a certain formal specification Si, which is straightforward to problem requirement P. And, Si is converted into an execute program using PAR method and PAR platform, and is validated by test. In order to support the method, further put forward an extended logic system and aided certified algorithm. The study will contribute to increase trustworthiness of Radl specification.

本项目基于我们在形式化软件规约Radl到可执行程序的软件(半)自动开发上的长期工作，进一步深入研究如何获取、验证与确认形式化规约Radl，它是当前软件自动化和需求工程中两个重要的问题。一、Radl规约的获取是通过设计受控自然语言SRL来描述问题需求，利用基于规则的方法将SRL通过转换生成为Radl,结合自然语言处理技术对生成过程的诸多难点寻求解决办法,由此研制从SRL到Radl的生成系统SRLtoRadl。并进一步探索运用范畴论框架建立SRLtoRadl生成系统可信性的理论模型。二、提出基于形式化推导的方法来验证与确认同一问题不同形式规约，基本思路是通过证明不同形式规约与问题需求P某个最为直截明了的形式化规约Si等价来达到的，而Si使用PAR方法和PAR平台转换为可执行程序，通过测试已经得到确认。为支持该方法，拟提出扩展的逻辑系统和辅助证明算法。该研究将有助于增强Radl规约的可信性。

形式化软件规约技术便于软件系统原型、分析、验证与最终的实现，是保证软件质量和提高软件生产率非常有用和重要的手段。本项目深入研究如何获取、验证与确认形式化规约Radl。为了减少或消除自然语言固有的歧义性，设计了一种受控自然语言--结构化需求语言(简称SRL)来描述问题需求。使用基于规则的方法，将结构化需求语言SRL通过分析-转换-综合三阶段生成为形式化软件规约Radl。设计并实现了结构化需求语言SRL到形式化软件规约Radl的生成系统SRLtoRadl，使用自然语言处理技术对生成过程中的诸多难点进行了处理。使用范畴论框架逐步的建立了SRLtoRadl生成系统生成过程的语义模型，它是SRLtoRadl生成系统高可靠性的理论基础。提出基于形式化推导的方法来验证与确认同一问题不同形式规约。为支持该方法，进而提出扩展的逻辑系统和辅助证明算法。该研究有助于增强Radl规约的可信性。