| 从用户需求到软件规约：一种问题变换的方法 |
| |
| 引用本文： | 李智,金芝.从用户需求到软件规约：一种问题变换的方法[J].软件学报,2013,24(5):961-976. |
| |
| 作者姓名： | 李智 金芝 |
| |
| 作者单位： | 广西师范大学计算机科学与信息工程学院, 广西 桂林 541004;高可信软件技术教育部重点实验室(北京大学), 北京 100871;高可信软件技术教育部重点实验室(北京大学), 北京 100871;北京大学信息科学技术学院 软件研究所, 北京 100871 |
| |
| 基金项目： | 国家重点基础研究发展计划(973)(2009CB320701); 国家自然科学基金(61262004); 广西自然科学基金(2012GXNSFCA-053010); “八桂学者”工程专项经费 |
| |
| 摘 要： | 研究的目的是在获取用户需求和领域描述的基础上规约出对软件规格的描述.提供了一种实现从用户需求到软件规约的平滑和可推理的变换方法.在深入研究问题框架方法的基础上,采用Hoare 的通信顺序进程语言CSP及Lai的最弱环境演算符实现了整个问题图的变换,且导出的软件规格是具有高抽象粒度的程序代码模型,能够被FDR模型检测工具所验证.该工作为实现嵌入式软件开发从需求到软件代码、文档的自动转化及验证等奠定了理论基础.此外,把该理论与模型检测工具FDR联合起来会有助于提高嵌入式软件开发的效率和准确性.
|
| 关 键 词： | 问题框架 通信顺序进程 领域和需求建模 最弱环境演算 软件规约 |
| 收稿时间： | 7/3/2012 12:00:00 AM |
| 修稿时间： | 2013/3/11 0:00:00 |
|
| 点击此处可从《软件学报》浏览原始摘要信息 |
|
点击此处可从《软件学报》下载全文 |
|
