“CCF形式化方法專委會走進(jìn)望安科技”研討會順利召開！
2025年7月11日，由中國計算機(jī)學(xué)會（CCF）主辦，中國計算機(jī)學(xué)會（CCF）形式化方法專業(yè)委員會和浙江望安科技有限公司聯(lián)合承辦的“‘智領(lǐng)未來’形式化方法產(chǎn)業(yè)應(yīng)用研討會——中國計算機(jī)學(xué)會（CCF）形式化方法專業(yè)委員會走進(jìn)望安科技”活動在浙江望安科技有限公司順利召開。
中國計算機(jī)學(xué)會（CCF）形式化方法專業(yè)委員會代表、柯橋區(qū)委組織部、柯橋區(qū)科學(xué)技術(shù)局、柯橋區(qū)大數(shù)據(jù)發(fā)展管理中心、金科橋科技城建設(shè)管理委員會、金柯橋數(shù)據(jù)有限公司、浙江大學(xué)形式化研究學(xué)者、浙江望安科技有限公司企業(yè)代表等約40人參加此次活動，旨在共同探討形式化方法產(chǎn)業(yè)應(yīng)用的新進(jìn)展、新機(jī)遇和新挑戰(zhàn)。
開幕式上，紹興金柯橋科技城建設(shè)管理委員會張志華主任發(fā)表致辭，對蒞臨的CCF形式化方法專委學(xué)者及所有參會者表示熱烈歡迎，并介紹了柯橋科技城的基本情況以及本次活動的深遠(yuǎn)意義，期待本次活動能為望安科技乃至整個區(qū)域的科技企業(yè)發(fā)展提供新的思路和方法。
CCF形式化方法專委會吳志林秘書長發(fā)表致辭，介紹了CCF形式化專委的情況，并向望安科技對本次活動的支持表達(dá)謝意，希望此次活動能夠增進(jìn)各位參會人員對形式化方法的了解，促進(jìn)學(xué)術(shù)界與產(chǎn)業(yè)界的深度融合。
趙永望教授作《望安科技形式化方法的探索與應(yīng)用》企業(yè)介紹。介紹中提到，望安科技是以“形式化驗證”和“安全認(rèn)證”為核心的安全服務(wù)及產(chǎn)品提供商，公司助力中國電子信息產(chǎn)品全面實現(xiàn)“高等級安全”。望安科技依托形式化驗證技術(shù)，以“形式化驗證解決方案”、“安全認(rèn)證解決方案”為業(yè)務(wù)主線，致力于為國家重大項目、關(guān)鍵系統(tǒng)及行業(yè)企業(yè)提供安全保障。公司憑借AI大模型底座，搭建了望安高等級安全SaaS平臺，從產(chǎn)品設(shè)計/開發(fā)階段的源頭到原生安全，到產(chǎn)品運營階段的國際/國家安全認(rèn)證背書，實現(xiàn)全生命周期的高等級安全，平臺具備原生安全開發(fā)工具 W-MetaSec、形式化建模驗證工具 W-Cert、全景圖 Secinfo、認(rèn)證工具 W-Caas等，為企業(yè)提供一站式安全認(rèn)證服務(wù)。
在專家報告環(huán)節(jié)，CCF會士、北京航空航天大學(xué)計算機(jī)學(xué)院博士生導(dǎo)師馬殿富教授作《從安全關(guān)鍵軟件看復(fù)雜軟件系統(tǒng)開發(fā)與形式驗證技術(shù)》主題報告，分享了安全關(guān)鍵軟件在復(fù)雜軟件系統(tǒng)開發(fā)中的重要性及形式化驗證技術(shù)的應(yīng)用。近年來，他主要研究安全關(guān)鍵軟件建模、開發(fā)與形式驗證方法研究，從事基于RISCV的CPU設(shè)計與形式證明方法研究、ARINGC653操作系統(tǒng)開發(fā)與形式驗證方法研究、以及模型語言Lustre及Scade的編譯開發(fā)與形式證明方法研究。
北京郵電大學(xué)網(wǎng)絡(luò)空間安全學(xué)院博士生導(dǎo)師李暉教授作《密碼協(xié)議形式化分析技術(shù)研究》主題報告，闡述了密碼協(xié)議及其分析方法，說明使用形式化方法代替人工方法對密碼協(xié)議進(jìn)行系統(tǒng)化分析的必要性。她以近年來提出的替代文本密碼的登錄方式為目標(biāo)的快速在線認(rèn)證協(xié)議FIDO中的統(tǒng)一認(rèn)證框架（UAF）和驗證OpenSSL協(xié)議握手過程的實現(xiàn)是否符合TLS1.3對狀態(tài)機(jī)的要求為例，講解了密碼協(xié)議安全性分析及一致性分析的主要思路。
南京航空航天大學(xué)計算機(jī)學(xué)院博士生導(dǎo)師楊志斌教授作《大模型增強(qiáng)的安全關(guān)鍵軟件模型驅(qū)動開發(fā)與驗證方法》主題報告，聚焦大模型增強(qiáng)的模型驅(qū)動開發(fā)與驗證方法，介紹了團(tuán)隊近幾年來將大模型技術(shù)融入航空航天關(guān)鍵軟件模型驅(qū)動開發(fā)與驗證過程的初步探索，主要包括大模型增強(qiáng)的模型驅(qū)動安全分析、基于大語言模型的SysML建模、基于大模型的安全關(guān)鍵軟件架構(gòu)建模、基于大模型的時序邏輯公式生成、SCADE模型驗證與測試的智能化增強(qiáng)等方面。
上海海洋大學(xué)信息學(xué)院碩士生導(dǎo)師，軟件工程系副主任張文博教授作《海洋學(xué)科距離形式化方法還有多遠(yuǎn)？》主題報告，詳細(xì)介紹了上海海洋大學(xué)數(shù)字海洋研究所近年來在海洋防災(zāi)減災(zāi)、海洋中尺度現(xiàn)象檢測、海冰解譯、海底視覺、海洋環(huán)境評估、海上風(fēng)電等方面的研究工作，探討未來海洋學(xué)科與形式化方法深度融合的路徑。
專題報告后，專家們與參會嘉賓開展研討交流，大家就形式化方法在不同領(lǐng)域的應(yīng)用前景、技術(shù)挑戰(zhàn)及未來發(fā)展方向等問題進(jìn)行了深入探討，現(xiàn)場氣氛熱烈，思想碰撞不斷，研討會取得圓滿成功。
