2024年5月31日，由新疆师范高等专科学校主办，中国计算机协会（CCF）形式化方法专委会走进高校、“数字新时代 信创筑未来”科学文化传播研讨会在新疆师范高等专科学校亚心校区举行。来自西南大学、西北工业大学、华东师范大学、国防科技大学、中国科学院软件所等单位CCF形式化方法专委会委员走进高校，带来了五场精彩的学术报告。信息科学与技术学院以及职业教育学院的师生240余人参加了此次活动。
    此次研讨会由中共中央组织部第11批援疆专家、湖南大学金融与统计学院教授、博士生导师、我校科研处负责人倪青山主持。校党委副书记、校长木开依•加尔肯别克同志致开幕辞，表达了对CCF形式化方法专委会的感谢，以及对专家亲临我校做学术报告的欢迎。随后，CCF形式化方法专委会副主任董威教授代表专委会致辞，介绍了专委会的情况及此次活动的目的。

      
 
                  与会领导和专家合影

      
  
                   会议现场

    会上，国家特聘专家、西南大学计算机学院教授、博士生导师、西南大学软件理论与系统团队负责人、软件研究与创新中心（RISE）主任刘志明做了题为《逻辑思维与计算思维并兼谈机器智能的能力》的主旨发言。他深入探讨了数理逻辑，计算理论和程序语言的基本概念和思想，揭示数理逻辑是计算机科学和系统的天然基础，通过数理逻辑，计算模型和程序语言的统一性理论，浅谈在推理和思维中自然语言的局限性和符号化形式语言的必要性，基于哥德尔不完备定理，从哲学层面说明人的心智和人工智能（AI）能力范围的区别。尽管AI取得了显著进展，但也不具备类似于物理学中牛顿定律的科学基础。他认为，目前人类的心智和意识仍然是独特的，并且在可预见的未来，AI不太可能具有人类的心智能力。随着技术的发展，人类将逐步建立AI的科学基础，解答AI的能力范围、可解释性以及AI是否具备推理和规划能力等问题。自然，与其他科技一样，AI具有广泛且强大的有益于人类的能力和作用，但如果使用不当，同样也可能给人类带来广泛且严重的破坏。

      
 
                   刘志明教授作报告

    西北工业大学软件学院教授，博士生导师， IEEE高级会员、可靠性性协会执委会委员（2018-2020）、西安分会主席，CCF杰出会员董云卫教授做了题为《智能软件工程理论概述》的报告，介绍了以大语言模型为代表的生成式神经元网络技术的快速发展和逐步应用，软件开发模式也发生了巨大的变化，对软件理论和工程实践技术迎来巨大的变革和前所未有的挑战，传统软件开发技术将被替代，软件工程师的能力培养和工作角色也将发生巨大变革。依据软件技术方法发展脉络，介绍不同阶段软件开发技术及其形态的演化过程。重点介绍了基于深度学习软件智能化开发方法的内涵及其技术思想，软件开发流程及其活动。最后讨论了智能软件工程教育面临的一些技术挑战和热点问题，并对软件工程学科技术发展趋势进行展望。

       
 
                    董云卫教授作报告

    中共中央组织部第11批援疆专家、华东师范大学软件工程学院副教授、CCF嵌入式专委会、形式化方法专委会委员郭建做题为《基于PC-ABAC模型的Linux安全文件系统》的报告，介绍了随着信息技术的高速发展，数据和资源的规模呈现爆发式增长，安全性逐渐成为信息系统领域的重要主题。访问控制机制被认为是保证数据共享和系统安全性的一项重要手段，针对基于属性访问控制实施过程中出现的问题，介绍了基于策略限制的属性访问控制（PC-ABAC）的形式化模型，通过对属性和访问控制策略的形式化定义，结合满足性理论，利用求解器对属性和策略进行安全性验证。在 Linux 文件系统中部署PC-ABAC 模型，实现了对 Linux 文件系统的安全访问控制。

       
 
                    郭建副教授作报告

    国防科技大学计算机学院教授、博士生导师、CCF形式化方法专委会副主任董威教授的“人机物融合计算技术及应用”报告，介绍了人机物融合系统已被认为是未来信息系统发展的主要形态，软件是三元融合的核心，“软件定义一切”已成为趋势。探讨了人机物融合计算中人机物融合系统的发展历程和特点，介绍了体系架构、系统建模、代码生成、验证等技术，以及人机物融合系统在多个领域的应用前景。

      
 
                    董威教授作报告

    中国科学院软件研究所基础软件与系统重点实验室（计算机科学国家重点实验室）研究员，博士生导师、CCF形式化方法专委会秘书长吴志林就《计算机软硬件基础设施的形式化验证》进行了深入的报告，介绍了一种基于数学推理的验证计算机系统的理论和方法——形式化方法。形式化验证技术是采用逻辑推理的手段来保障计算机系统的正确性与安全性，已经广泛用于计算机软硬件基础设施的验证，包括芯片设计、操作系统与编译器、网络与分布式协议等。介绍了计算机软硬件基础设施的形式化验证国内外相关工作，以及对形式化方法在未来的应用进行了展望。

      
 
                   吴志林教授作报告

    在互动交流环节，与会专家与我校师生进行了热烈的讨论与交流，为师生的学术研究与教育实践提供了宝贵的指导。最后，信息科学与技术学院宋彬院长对本次研讨会进行总结，并对参与本次研讨会的专家学者再次表达了诚挚的感谢。
    本次研讨会由中共中央组织部第11批援疆专家、华东师范大学软件工程学院副教授、CCF嵌入式专委会、形式化方法专委会委员郭建策划发起，为我校师生近距离接触国内高水平大学及科研院所的专家提供了非常好的交流平台，促进了我校师生了解国内外在形式化方法、人工智能、大模型等领域的最新发展，推动了我校学术水平的提高。 （杨瑞红）

来源：产新网