软件测试与开发方法的基础研究

　　发展历程：1994年，李未首次建立了在软件需求说明层次错误定位和需求说明修正的形式演算系统，即R-演算系统原型。在2002、03年的论文中对94年的R-演算系统进行了重大改进，并证明了R-演算系统的可达性、可靠性和完全性。在2006年将R-演算系统推广到一阶语言的任意公式集合上，并证明了此时R-演算仍然具有可达性、可靠性和完全性。

　　主要目标：研究和发展软件测试和修改的机械化技术，以提高测试效率，缩短软件生产周期。 研究合理的软件开发方法所需满足的基本特征，从而增强软件生产可靠性，降低开发成本。

　　研究内容：给出软件错误的形式化定义，研究软件错误修正的基本原则，建立形式化的软件错误定位和修正系统，证明其可靠性和完全性，为软件的测试和修正提供一个理论基础。
　　给出构造性的形式化定义，设计构造性描述语言以描述软件开发方法，并在此基础之上总结合理的软件开发方法所需满足的基本特征。

　　学术成果：这项研究成果在LNCS、《中国科学》、《软件学报》、JCST上发表了6篇论文，在德国不来梅大学、萨尔布吕肯大学、哈根大学、帕德波恩大学、英国爱丁堡大学、美国明尼苏达大学和日本东京大学做过多次专题报告，并于2006年被英国计算机学会会刊《The Computer Journal》作为特约论文接受，将于2007年发表。