2025年7月11日，由中國(guó)計(jì)算機(jī)學(xué)會(huì)(CCF)主辦，中國(guó)計(jì)算機(jī)學(xué)會(huì)(CCF)形式化方法專(zhuān)業(yè)委員會(huì)和浙江望安科技有限公司聯(lián)合承辦的“‘智領(lǐng)未來(lái)’形式化方法產(chǎn)業(yè)應(yīng)用研討會(huì)——中國(guó)計(jì)算機(jī)學(xué)會(huì)(CCF)形式化方法專(zhuān)業(yè)委員會(huì)走進(jìn)望安科技”活動(dòng)在浙江望安科技有限公司順利召開(kāi)。

　　中國(guó)計(jì)算機(jī)學(xué)會(huì)(CCF)形式化方法專(zhuān)業(yè)委員會(huì)代表、柯橋區(qū)委組織部、柯橋區(qū)科學(xué)技術(shù)局、柯橋區(qū)大數(shù)據(jù)發(fā)展管理中心、金科橋科技城建設(shè)管理委員會(huì)、金柯橋數(shù)據(jù)有限公司、浙江大學(xué)形式化研究學(xué)者、浙江望安科技有限公司企業(yè)代表等約40人參加此次活動(dòng)，旨在共同探討形式化方法產(chǎn)業(yè)應(yīng)用的新進(jìn)展、新機(jī)遇和新挑戰(zhàn)。

　　開(kāi)幕式上，紹興金柯橋科技城建設(shè)管理委員會(huì)張志華主任發(fā)表致辭，對(duì)蒞臨的CCF形式化方法專(zhuān)委學(xué)者及所有參會(huì)者表示熱烈歡迎，并介紹了柯橋科技城的基本情況以及本次活動(dòng)的深遠(yuǎn)意義，期待本次活動(dòng)能為望安科技乃至整個(gè)區(qū)域的科技企業(yè)發(fā)展提供新的思路和方法。

　　CCF形式化方法專(zhuān)委會(huì)吳志林秘書(shū)長(zhǎng)發(fā)表致辭，介紹了CCF形式化專(zhuān)委的情況，并向望安科技對(duì)本次活動(dòng)的支持表達(dá)謝意，希望此次活動(dòng)能夠增進(jìn)各位參會(huì)人員對(duì)形式化方法的了解，促進(jìn)學(xué)術(shù)界與產(chǎn)業(yè)界的深度融合。

　　趙永望教授作《望安科技形式化方法的探索與應(yīng)用》企業(yè)介紹。介紹中提到，望安科技是以“形式化驗(yàn)證”和“安全認(rèn)證”為核心的安全服務(wù)及產(chǎn)品提供商，公司助力中國(guó)電子信息產(chǎn)品全面實(shí)現(xiàn)“高等級(jí)安全”。望安科技依托形式化驗(yàn)證技術(shù)，以“形式化驗(yàn)證解決方案”、“安全認(rèn)證解決方案”為業(yè)務(wù)主線，致力于為國(guó)家重大項(xiàng)目、關(guān)鍵系統(tǒng)及行業(yè)企業(yè)提供安全保障。公司憑借AI大模型底座，搭建了望安高等級(jí)安全SaaS平臺(tái)，從產(chǎn)品設(shè)計(jì)/開(kāi)發(fā)階段的源頭到原生安全，到產(chǎn)品運(yùn)營(yíng)階段的國(guó)際/國(guó)家安全認(rèn)證背書(shū)，實(shí)現(xiàn)全生命周期的高等級(jí)安全，平臺(tái)具備原生安全開(kāi)發(fā)工具 W-MetaSec、形式化建模驗(yàn)證工具 W-Cert、全景圖 Secinfo、認(rèn)證工具 W-Caas等，為企業(yè)提供一站式安全認(rèn)證服務(wù)。

　　在專(zhuān)家報(bào)告環(huán)節(jié)，CCF會(huì)士、北京航空航天大學(xué)計(jì)算機(jī)學(xué)院博士生導(dǎo)師馬殿富教授作《從安全關(guān)鍵軟件看復(fù)雜軟件系統(tǒng)開(kāi)發(fā)與形式驗(yàn)證技術(shù)》主題報(bào)告，分享了安全關(guān)鍵軟件在復(fù)雜軟件系統(tǒng)開(kāi)發(fā)中的重要性及形式化驗(yàn)證技術(shù)的應(yīng)用。近年來(lái)，他主要研究安全關(guān)鍵軟件建模、開(kāi)發(fā)與形式驗(yàn)證方法研究，從事基于RISCV的CPU設(shè)計(jì)與形式證明方法研究、ARINGC653操作系統(tǒng)開(kāi)發(fā)與形式驗(yàn)證方法研究、以及模型語(yǔ)言Lustre及Scade的編譯開(kāi)發(fā)與形式證明方法研究。

　　北京郵電大學(xué)網(wǎng)絡(luò)空間安全學(xué)院博士生導(dǎo)師李暉教授作《密碼協(xié)議形式化分析技術(shù)研究》主題報(bào)告，闡述了密碼協(xié)議及其分析方法，說(shuō)明使用形式化方法代替人工方法對(duì)密碼協(xié)議進(jìn)行系統(tǒng)化分析的必要性。她以近年來(lái)提出的替代文本密碼的登錄方式為目標(biāo)的快速在線認(rèn)證協(xié)議FIDO中的統(tǒng)一認(rèn)證框架(UAF)和驗(yàn)證OpenSSL協(xié)議握手過(guò)程的實(shí)現(xiàn)是否符合TLS1.3對(duì)狀態(tài)機(jī)的要求為例，講解了密碼協(xié)議安全性分析及一致性分析的主要思路。

　　南京航空航天大學(xué)計(jì)算機(jī)學(xué)院博士生導(dǎo)師楊志斌教授作《大模型增強(qiáng)的安全關(guān)鍵軟件模型驅(qū)動(dòng)開(kāi)發(fā)與驗(yàn)證方法》主題報(bào)告，聚焦大模型增強(qiáng)的模型驅(qū)動(dòng)開(kāi)發(fā)與驗(yàn)證方法，介紹了團(tuán)隊(duì)近幾年來(lái)將大模型技術(shù)融入航空航天關(guān)鍵軟件模型驅(qū)動(dòng)開(kāi)發(fā)與驗(yàn)證過(guò)程的初步探索，主要包括大模型增強(qiáng)的模型驅(qū)動(dòng)安全分析、基于大語(yǔ)言模型的SysML建模、基于大模型的安全關(guān)鍵軟件架構(gòu)建模、基于大模型的時(shí)序邏輯公式生成、SCADE模型驗(yàn)證與測(cè)試的智能化增強(qiáng)等方面。

　　上海海洋大學(xué)信息學(xué)院碩士生導(dǎo)師，軟件工程系副主任張文博教授作《海洋學(xué)科距離形式化方法還有多遠(yuǎn)?》主題報(bào)告，詳細(xì)介紹了上海海洋大學(xué)數(shù)字海洋研究所近年來(lái)在海洋防災(zāi)減災(zāi)、海洋中尺度現(xiàn)象檢測(cè)、海冰解譯、海底視覺(jué)、海洋環(huán)境評(píng)估、海上風(fēng)電等方面的研究工作，探討未來(lái)海洋學(xué)科與形式化方法深度融合的路徑。

　　專(zhuān)題報(bào)告后，專(zhuān)家們與參會(huì)嘉賓開(kāi)展研討交流，大家就形式化方法在不同領(lǐng)域的應(yīng)用前景、技術(shù)挑戰(zhàn)及未來(lái)發(fā)展方向等問(wèn)題進(jìn)行了深入探討，現(xiàn)場(chǎng)氣氛熱烈，思想碰撞不斷，研討會(huì)取得圓滿成功。