“软件”是现代社会基础设施的“灵魂”，“软件定义一切”是当前的一个热门话题。软件需求工程是决定一个软件项目完成质量好坏的重要手段，即使将来人工智能可以通过自动化编程来取代人工编程过程，软件需求工程仍将是软件工程研究和实践的核心问题，因此迫切需要研究和开发软件需求工程的理论和技术。
软件开发中一个普遍接受的观点是，形式化方法在验证现实世界中的需求时遇到困难，而非形式化的方法在识别和表征需求中的形式化结构也同样面临困难。计算机处理和解决的问题常处于非形式化的现实世界，而所提供的解决方案本质上是具有形式化属性的机器，因此这两种截然对立的矛盾在软件开发中总是存在。李智教授课题组与英国开放大学、北京大学的著名学者合作，研究成果主要在形式化理论研究、半形式化应用研究以及把两者结合起来的计算机辅助工具支持等三个方面进行了一系列卓有成效的研究。
1. 形式化研究方面：提供了一种实现从用户需求到软件规约的平滑和可推理的变换方法，即采用Hoare的通信顺序进程语言CSP及Lai的最弱环境演算符实现了整个问题图的变换，且导出的软件规格是具有高抽象粒度的程序代码模型，能够被FDR模型检测工具所验证。这种CSP 表示的软件规约易于用编程语言实现或被映射到相应的软件架构上，为实现嵌入式软件开发从需求到软件代码、文档的自动转化及验证等奠定了理论基础。这部分成果发表在国内软件领域权威期刊《软件学报》第24卷第5期上，论文合著者是国家杰出青年基金项目获得者、中国计算机学会软件工程专委会主任、北京大学金芝教授。
2. 半形式化方面：通过使用图文法对杰克逊在问题框架中提出的问题渐变进行了形式化，提出并实现了如何系统地将用户需求变换为软件规约。本工作在需求工程研究中做到问题领域行为的形式化与需求表征的非形式化研究的兼顾，即做到两者兼容并蓄的学术研究思想。软件工程著名学者Pamela Zave博士(现任美国普林斯顿大学计算机系研究员)该工作评价认为，“它划清了问题框架研究中哪些要形式化和哪些不必形式化之间的界限”。
3. 工具支持方面：本成果为软件开发过程提供一整套计算机辅助需求分析工具，对推动杰克逊问题框架方法从理论走向实际应用、更加好地进行经验评估提供了技术支持。随后申请并获得的8项软件著作权，都是直接受到本工作的启发和推动，因此，其影响力主要体现在推动软件工程方法从理论走向实际应用和经验评估、评价等方面。
总之，李智教授获得国家自然科学基金项目2项、省部级项目4项，发表学术论文20余篇(SCI、EI论文17篇，CCF期刊和会议论文13篇，其中3次获得国际学术会议最佳论文奖)，做会议邀请报告4次，申请并获得软件著作权8项(1项已经转让)及授权专利1项，申请发明专利2项(已受理)。获得并主持教育部产学合作协同育人项目（腾讯资助）1项、地厅级教改项目1项、校级教改项目3项、获得校级教学成果一等奖1项，培养的硕士研究生有5人继续在南京大学、北京航天航空大学、天津大学、武汉大学和湖南大学攻读博士学位。
