5月31日，由新疆師范高等專科學(xué)校主辦的“數(shù)字新時代 信創(chuàng)筑未來”科學(xué)文化傳播研討會在亞心校區(qū)舉行。來自西南大學(xué)、西北工業(yè)大學(xué)、華東師范大學(xué)、國防科技大學(xué)、中國科學(xué)院軟件所等單位CCF形式化方法專委會委員走進高校，帶來了五場精彩的學(xué)術(shù)報告。我校信息科學(xué)與技術(shù)學(xué)院以及職業(yè)教育學(xué)院的師生240余人參加了此次活動。
此次研討會由中共中央組織部第11批援疆專家、湖南大學(xué)金融與統(tǒng)計學(xué)院教授、博士生導(dǎo)師、我?？蒲刑庁撠?zé)人倪青山主持。校黨委副書記、校長木開依·加爾肯別克同志致開幕辭，表達了對CCF形式化方法專委會的感謝，以及對專家親臨我校做學(xué)術(shù)報告的歡迎。隨后，CCF形式化方法專委會副主任董威教授代表專委會致辭，介紹了專委會的情況及此次活動的目的。
與會領(lǐng)導(dǎo)和專家合影
會議現(xiàn)場
會上，西南大學(xué)計算機學(xué)院教授、博士生導(dǎo)師、西南大學(xué)軟件理論與系統(tǒng)團隊負責(zé)人、軟件研究與創(chuàng)新中心（RISE）主任劉志明做了題為《邏輯思維與計算思維并兼談機器智能的能力》的主旨發(fā)言。他深入探討了數(shù)理邏輯，計算理論和程序語言的基本概念和思想，揭示數(shù)理邏輯是計算機科學(xué)和系統(tǒng)的天然基礎(chǔ)，通過數(shù)理邏輯，計算模型和程序語言的統(tǒng)一性理論，淺談在推理和思維中自然語言的局限性和符號化形式語言的必要性，基于哥德爾不完備定理，從哲學(xué)層面說明人的心智和人工智能（AI）能力范圍的區(qū)別。盡管AI取得了顯著進展，但也不具備類似于物理學(xué)中牛頓定律的科學(xué)基礎(chǔ)。他認為，目前人類的心智和意識仍然是獨特的，并且在可預(yù)見的未來，AI不太可能具有人類的心智能力。隨著技術(shù)的發(fā)展，人類將逐步建立AI的科學(xué)基礎(chǔ)，解答AI的能力范圍、可解釋性以及AI是否具備推理和規(guī)劃能力等問題。自然，與其他科技一樣，AI具有廣泛且強大的有益于人類的能力和作用，但如果使用不當(dāng)，同樣也可能給人類帶來廣泛且嚴重的破壞。
劉志明教授作報告
西北工業(yè)大學(xué)軟件學(xué)院教授，博士生導(dǎo)師， IEEE高級會員、可靠性協(xié)會執(zhí)委會委員（2018-2020）、西安分會主席，CCF杰出會員董云衛(wèi)教授做了題為《智能軟件工程理論概述》的報告，介紹了以大語言模型為代表的生成式神經(jīng)元網(wǎng)絡(luò)技術(shù)的快速發(fā)展和逐步應(yīng)用，軟件開發(fā)模式也發(fā)生了巨大的變化，對軟件理論和工程實踐技術(shù)迎來巨大的變革和前所未有的挑戰(zhàn)，傳統(tǒng)軟件開發(fā)技術(shù)將被替代，軟件工程師的能力培養(yǎng)和工作角色也將發(fā)生巨大變革。依據(jù)軟件技術(shù)方法發(fā)展脈絡(luò)，介紹不同階段軟件開發(fā)技術(shù)及其形態(tài)的演化過程。重點介紹了基于深度學(xué)習(xí)軟件智能化開發(fā)方法的內(nèi)涵及其技術(shù)思想，軟件開發(fā)流程及其活動。最后討論了智能軟件工程教育面臨的一些技術(shù)挑戰(zhàn)和熱點問題，并對軟件工程學(xué)科技術(shù)發(fā)展趨勢進行展望。
董云衛(wèi)教授作報告
中共中央組織部第11批援疆專家、華東師范大學(xué)軟件工程學(xué)院副教授、CCF嵌入式專委會、形式化方法專委會委員郭建做題為《基于PC-ABAC模型的Linux安全文件系統(tǒng)》的報告，介紹了隨著信息技術(shù)的高速發(fā)展，數(shù)據(jù)和資源的規(guī)模呈現(xiàn)爆發(fā)式增長，安全性逐漸成為信息系統(tǒng)領(lǐng)域的重要主題。訪問控制機制被認為是保證數(shù)據(jù)共享和系統(tǒng)安全性的一項重要手段，針對基于屬性訪問控制實施過程中出現(xiàn)的問題，介紹了基于策略限制的屬性訪問控制（PC-ABAC）的形式化模型，通過對屬性和訪問控制策略的形式化定義，結(jié)合滿足性理論，利用求解器對屬性和策略進行安全性驗證。在 Linux 文件系統(tǒng)中部署PC-ABAC 模型，實現(xiàn)了對 Linux 文件系統(tǒng)的安全訪問控制。
郭建副教授作報告
國防科技大學(xué)計算機學(xué)院教授、博士生導(dǎo)師、CCF形式化方法專委會副主任董威教授的“人機物融合計算技術(shù)及應(yīng)用”報告，介紹了人機物融合系統(tǒng)已被認為是未來信息系統(tǒng)發(fā)展的主要形態(tài)，軟件是三元融合的核心，“軟件定義一切”已成為趨勢。探討了人機物融合計算中人機物融合系統(tǒng)的發(fā)展歷程和特點，介紹了體系架構(gòu)、系統(tǒng)建模、代碼生成、驗證等技術(shù)，以及人機物融合系統(tǒng)在多個領(lǐng)域的應(yīng)用前景。
董威教授作報告
中國科學(xué)院軟件研究所基礎(chǔ)軟件與系統(tǒng)重點實驗室（計算機科學(xué)國家重點實驗室）研究員，博士生導(dǎo)師、CCF形式化方法專委會秘書長吳志林就《計算機軟硬件基礎(chǔ)設(shè)施的形式化驗證》進行了深入的報告，介紹了一種基于數(shù)學(xué)推理的驗證計算機系統(tǒng)的理論和方法——形式化方法。形式化驗證技術(shù)是采用邏輯推理的手段來保障計算機系統(tǒng)的正確性與安全性，已經(jīng)廣泛用于計算機軟硬件基礎(chǔ)設(shè)施的驗證，包括芯片設(shè)計、操作系統(tǒng)與編譯器、網(wǎng)絡(luò)與分布式協(xié)議等。介紹了計算機軟硬件基礎(chǔ)設(shè)施的形式化驗證國內(nèi)外相關(guān)工作，以及對形式化方法在未來的應(yīng)用進行了展望。
吳志林教授作報告
在互動交流環(huán)節(jié)，與會專家與我校師生進行了熱烈的討論與交流，為師生的學(xué)術(shù)研究與教育實踐提供了寶貴的指導(dǎo)。最后，信息科學(xué)與技術(shù)學(xué)院宋彬院長對本次研討會進行總結(jié)，并對參與本次研討會的專家學(xué)者再次表達了誠摯的感謝。
此次活動為我校師生近距離接觸國內(nèi)高水平大學(xué)及科研院所的專家提供了非常好的交流平臺，促進了我校師生了解國內(nèi)外在形式化方法、人工智能、大模型等領(lǐng)域的最新發(fā)展，推動了我校學(xué)術(shù)水平的提高。
供稿：新疆師范高等?？茖W(xué)?？茀f(xié)
責(zé)任編輯：劉旭歡
