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