摘要：人类社会正在从“信息时代”进入“智能时代”。新一代信息技术、人工智能等产业作为新的增长引擎，已上升为国家战略。首都师范大学信息工程学院“可信软件工程”团队在可信软件与人工智能人才培养和前沿科学研究领域深耕多年，瞄准关键基础软件自主可控的国家需求，聚焦产学研一体
人类社会正在从“信息时代”进入“智能时代”。新一代信息技术、人工智能等产业作为新的增长引擎，已上升为国家战略。首都师范大学信息工程学院“可信软件工程”团队在可信软件与人工智能人才培养和前沿科学研究领域深耕多年，瞄准关键基础软件自主可控的国家需求，聚焦产学研一体化赋能和科技成果转化，为推动“新质生产力”发展做出了首都师大应有的贡献。
首都师范大学信息工程学院“可信软件工程”团队部分教师
一、抱朴守拙：深耕“形式化方法”聚焦关键软件自主可控
面向未来智能世界，软件是核心更是基础。“C++之父”本贾尼·斯特劳斯特卢普提出“软件定义世界”的观点，中国科学院院士梅宏教授也常在国内普及“软件定义未来世界”的理念。谈起信息工程学院“可信软件工程”团队的建立初衷，团队创始人关永教授回忆道：“最初决定建立可信软件工程团队是想解决科研同质化问题。如何选择一个有希望的研究方向？可以从以下几个方面入手：一是研究方向需契合国家发展需要，兼顾从0到1的基础研究与从1到100的工程创新相结合；二是对标国际前瞻领域与发展方向；三是研究方向与内容应具有一定的持久性，不能昙花一现。按照以上规则，我们从2008年初开始，将团队的主要研究方向定位到形式化验证领域，经过16年的不断迭代，逐渐将人工智能、机器人的安全做为形式化验证的主要对象，形成了如今在国际上有自己独特影响力的可信人工智能研究队伍。”
当前，我国软件行业依然面临基础创新能力不足、对外依存度大、与行业融合应用不够深入等问题。“可信软件工程”团队在机器定理证明和软件形式化验证方面不断探索，研究领域包括可信软件理论、软件形式化建模与验证、数学理论形式化、模型驱动开发与测试方法等方面，在探索关键基础软件自主可控相关技术的道路上逐渐形成了自己的独特积累与优势。
几何代数形式化定理库被国际最著名的定理证明系统HOL Light官方收录并向全球发布
信息工程学院获批国家级、省部级重点实验室
北京市科学技术研究院副院长、首都师范大学信息工程学院原院长、团队负责人施智平教授介绍，形式化方法是可信软件工程中最重要的技术之一，它是唯一可以在理论上证明软件正确性的方法。形式化方法常常应用在对安全性要求非常高的软件和领域中，例如飞机制造、国防和人造卫星等领域。然而使用形式化方法的代价也很高，有时候为确保一行代码的逻辑性和准确性甚至需要二十至三十行形式化代码去验证。“可能这个研究方向并不是很热，也不能短平快的出成果，学习和研究确实很难。但正是因为研究的人少又是国家战略所需，我们就更要坚持，做科研需要抱朴守拙的精神，我们一定要把定理证明坚持做下去。”施智平教授谈到。
团队负责人施智平教授
信息工程学院“可信软件工程”团队自2008年就专注于高可靠嵌入式系统方向，逐步扩展到对形式化方法的研究，在工程数学形式化和机器人操作系统验证方面取得了有国际影响力的成果，研发了国内规模最大的数学理论定理证明程序库，多个程序库被国际主流定理证明器HOL4和HOL Light接收并发布，在国际上率先提出基于几何代数、分析动力学理论的机器人运动学和动力学形式化建模理论，出版了四本专著，是国际上研发工程数学形式化定理证明程序库最多的团队之一。基于多年的研究基础，团队承担了我国自主开发的工业操作系统形式化验证等任务，采用定理证明方法验证了操作系统任务同步与通信模块、安全分区控制模块的正确性与安全性，在已进行大量测试的代码中发现了多种问题，并与开发人员共同完成了问题的修复，提升了该操作系统关键模块的代码质量、可靠性与安全性。团队牵头完成的成果三次获得北京市科学技术二等奖。
机器定理证明和软件形式化验证研究成果三次获北京市科学技术二等奖
机器定理证明和软件形式化验证方向出版的专著
二、奋发有为：产学研融合赋能新质生产力发展
在新时代背景下，新质生产力的形成离不开软件和人工智能技术的支持。“可信软件工程”团队心系国家产业发展需求，积极践行产学研融合发展理念，承担了科技部、航天院所、华为、上海商飞等许多攻关项目。
基于轻型协作机器人的电源断路器全自动检测系统
国产大飞机完成商业首飞至今已满周年，其中就有我校信息工程学院“可信软件工程”团队所做出的贡献。邵振洲教授，针对飞机 EE 舱工作空间小，操作不便等难题，为上海飞机制造有限公司研制了基于轻型协作机器人的电源断路器全自动检测系统。这是国产大型客机迄今为止第一套上机运行的全自动检测系统。同时，邵振洲教授还以第一起草人制定工业机器人的通用驱动模块接口国际标准，2021年2月正式分布，相关成果获得2024年度北京机械工业科技进步二等奖。团队与北京控制工程研究所开展深度合作，成功获批北京市科技新星交叉项目（面向复杂协同操作的空间稳定基准建立与控制技术研究），该项目面向未来空间任务的国家重大需求，瞄准高精密航天器在轨组装对平台与机械臂协同配合精度的要求，从操作过程的位姿感知、机械臂空间规划与控制、航天器基准的稳定保持与精确指向、基准与机械臂协同控制四个方面开展研究，为我国空间基础高品质设施建设提供理论方法支撑。
高精密航天器在轨组装
为实现软件自主可控，提高基础工业软件设计，王瑞教授和清华大学合作，为华为的车载软件系统研制了一套可建模、仿真和代码生成的开发工具，该工具能够在设计阶段验证系统的正确性，缩减了开发周期和成本，提高了系统的安全性，现已交付华为公司，在新能源汽车软件系统开发领域解决了原有过分依赖国外基础开发环境的困境。刘卉教授与农科院智能装备技术研究中心合作，研发基于北斗的农业机械自动导航作业关键技术，重点在速度自适应的农机作业纯路径跟踪控制方法、农田全区域覆盖作业路径优化规划方法和农机北斗自动导航效果评估等3项关键方法和技术方面做出创新性贡献，她参与研制的具有自主知识产权的液压转向和电机转向两类农机北斗自动导航产品已实现产业化，产品已累计推广应用两千余套，作业面积870多万亩，成果获2020年国家科技进步二等奖。
基于北斗的农业机械自动导航作业关键技术及应用项目获国家科技进步二等奖
在“人工智能+教育”领域，团队教师在智能教育、自然语言处理、知识工程以及面向教育服务的软件开发与维护方法等方面持续深耕，将科技成果向现实生产力进行转化。宋巍教授研究的作文评分和批改技术在科大讯飞语文作文智能评测系统中应用，是教育智能化的典型案例，目前应用在全国近三十个省市，评测作文逾7亿篇，已服务1.3万多所学校和2000多万学生。团队不仅在核心技术攻关上敢于啃硬骨头，同时也积极服务首都基础教育，服务乡村振兴，不忘初心，坚守首师姓“师”的初心使命。云桥学院于2015年由孙众教授创立，其主要宗旨是提升偏远乡村学校教师的信息技术教育应用能力。“云桥学院”之名意为基于云端环境，以在线课程和移动课程为依托，建立起高校师生和偏远农村教师的协同成长之桥。截止到2024年，云桥学院已连续十年，为全国25个省份343所农村学校近3万人次的农村教师提供服务。该公益项目先后获得全国教育创新博览会（教博会）SERVE奖；获批教育部首批教育信息化教学应用实践共同体项目；入选教育部中小学教师信息素养和教育教学能力提升优秀案例等。
云桥学院项目获得全国教育创新博览会（教博会）SERVE奖
2019年人工智能+教师教育国际研讨会
三、用心用情：着力培养可信软件和人工智能科技人才
学院在人才培养方面，紧扣时代发展需要，积极建立符合社会生产需要的人才培养模式，以“三全育人”工作机制为抓手，以“第一班主任”制度为平台，以“辅导员-班主任（导师）”协同育人工作模式为实践，用心用情，开展大学生思想政治教育工作。同时，团队教师主动探索，创新授课模式，发挥党建引领作用，在课程实践过程中贯彻课程思政“三化”改革，即课程思政专业化、课程思政融入化和课程思政实效化。形成重研讨、探究式、强实践的教学特色，实现以学生为主体的全过程育人方法。引导学生增强使命担当，提升文化自信，为全面建设社会主义现代化国家贡献青春力量。
科技创新驱动着科学技术快速发展，如何培养有创新意识的未来社会的建设者。首都师范大学信息工程学院“可信软件工程”团队给出了自己的探索。在人工智能创新实践型人才培养体系下，团队教师以学生的兴趣为重要驱动力，以学科竞赛为依托、实际任务为目标，紧密联系专业基础知识、加强学生的综合能力。设立各类面向本科生的科研项目、将竞赛和科研融入专业学习。信息工程学院2020级本科生邱宇轩通过参与导师团队的研究学习，取得非常大的进步。他说：“正是与导师团队的紧密合作，推动了自身能力的提升。”凭借出色的学术表现与创新能力，邱宇轩发表两篇高水平学术论文，获得了2024年校长奖学金一等奖，并保研至本校继续深造。未来，他将在首都师大信息工程学院“可信软件工程”团队中学习，为学术创新贡献青春力量。
信息工程学院教学副院长、团队成员陈文龙教授与学生讨论
“工科类院校实际上就是要培养实实在在对社会经济发展有用的创新型人才，无论是学生培养还是教师团队建设，都要服务于社会和国家的发展需求。”关永教授谈到。团队注重科教融合，将科研与教学紧密结合。通过开设高水平的系列课程和专题讲座，学生及时了解学科前沿知识，掌握最新的科研方法和技术。同时，积极引入实践基地资源，共签约13家实践基地。学院鼓励学生多到企业中进行实习实践，对于很多信工学子，尤其是专业型硕士，他们大多是三年在校内学习生活，一年在基地实习实践，“在实习过程中能够逐步了解社会所需，运用自己的专业知识解决实际问题，对我的帮助真的很大。”信息工程学院2020届硕士毕业生温兴森谈到，“我目前就职于蚂蚁集团，实习期间，可能会面临各种挑战和任务，这些经历将成为职业生涯中宝贵的财富。”在团队教师的培养下，学生不仅具有一定的学术功底，也在团队协作和沟通能力上有显著提升。
“第一班主任”召开主题班会
信息工程学院与北京市计算中心有限公司共建学生实践培养基地
多年来，首都师范大学信息工程学院“可信软件工程”团队坚持抱朴守拙做科研、奋发有为做服务、用心用情做教育，正是这样的坚持带动了学科建设水平的不断提高，随着教育部2024年博士点评审揭晓，首都师范大学信息工程学院成功获批软件工程一级学科博士学位授权点，这是首都师大几代信工师生坚韧不拔和勤奋开拓的结果。面向未来，首都师范大学信息工程学院“可信软件工程”团队将不忘初心，始终以国家的发展需求为目标，为首都和国家的科技发展和人才培养做出贡献。
编辑：王涵玉、张姝婷；责任编辑：陈巍文；审核：郭圆圆；图文来源：信息工程学院
感谢关永教授、王瑞教授及“可信软件工程”团队对于本文的大力支持
来源：首都师范大学
