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

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

项目编号： No.61363012

项目类型： 地区科学基金项目

立项/批准年度： 2013

项目学科： 自动化技术、计算机技术

项目作者： 王昌晶

作者单位： 江西师范大学

项目金额： 45万元

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

英文关键词： formal software specification；specification acquisition；specification verification and validation；category semantics；trustworthiness