“CCF形式化方法專委會走進望安科技”研討會順利召開

　　2025年7月11日，由中國計算機學會(CCF)主辦，中國計算機學會(CCF)形式化方法專業委員會和浙江望安科技有限公司聯合承辦的“‘智領未來’形式化方法產業應用研討會——中國計算機學會(CCF)形式化方法專業委員會走進望安科技”活動在浙江望安科技有限公司順利召開。

　　中國計算機學會(CCF)形式化方法專業委員會代表、柯橋區委組織部、柯橋區科學技術局、柯橋區大數據發展管理中心、金科橋科技城建設管理委員會、金柯橋數據有限公司、浙江大學形式化研究學者、浙江望安科技有限公司企業代表等約40人參加此次活動，旨在共同探討形式化方法產業應用的新進展、新機遇和新挑戰。

　　開幕式上，紹興金柯橋科技城建設管理委員會張志華主任發表致辭，對蒞臨的CCF形式化方法專委學者及所有參會者表示熱烈歡迎，并介紹了柯橋科技城的基本情況以及本次活動的深遠意義，期待本次活動能為望安科技乃至整個區域的科技企業發展提供新的思路和方法。

　　CCF形式化方法專委會吳志林秘書長發表致辭，介紹了CCF形式化專委的情況，并向望安科技對本次活動的支持表達謝意，希望此次活動能夠增進各位參會人員對形式化方法的了解，促進學術界與產業界的深度融合。

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

　　在專家報告環節，CCF會士、北京航空航天大學計算機學院博士生導師馬殿富教授作《從安全關鍵軟件看復雜軟件系統開發與形式驗證技術》主題報告，分享了安全關鍵軟件在復雜軟件系統開發中的重要性及形式化驗證技術的應用。近年來，他主要研究安全關鍵軟件建模、開發與形式驗證方法研究，從事基于RISCV的CPU設計與形式證明方法研究、ARINGC653操作系統開發與形式驗證方法研究、以及模型語言Lustre及Scade的編譯開發與形式證明方法研究。

　　北京郵電大學網絡空間安全學院博士生導師李暉教授作《密碼協議形式化分析技術研究》主題報告，闡述了密碼協議及其分析方法，說明使用形式化方法代替人工方法對密碼協議進行系統化分析的必要性。她以近年來提出的替代文本密碼的登錄方式為目標的快速在線認證協議FIDO中的統一認證框架(UAF)和驗證OpenSSL協議握手過程的實現是否符合TLS1.3對狀態機的要求為例，講解了密碼協議安全性分析及一致性分析的主要思路。

　　南京航空航天大學計算機學院博士生導師楊志斌教授作《大模型增強的安全關鍵軟件模型驅動開發與驗證方法》主題報告，聚焦大模型增強的模型驅動開發與驗證方法，介紹了團隊近幾年來將大模型技術融入航空航天關鍵軟件模型驅動開發與驗證過程的初步探索，主要包括大模型增強的模型驅動安全分析、基于大語言模型的SysML建模、基于大模型的安全關鍵軟件架構建模、基于大模型的時序邏輯公式生成、SCADE模型驗證與測試的智能化增強等方面。

　　上海海洋大學信息學院碩士生導師，軟件工程系副主任張文博教授作《海洋學科距離形式化方法還有多遠?》主題報告，詳細介紹了上海海洋大學數字海洋研究所近年來在海洋防災減災、海洋中尺度現象檢測、海冰解譯、海底視覺、海洋環境評估、海上風電等方面的研究工作，探討未來海洋學科與形式化方法深度融合的路徑。

　　專題報告后，專家們與參會嘉賓開展研討交流，大家就形式化方法在不同領域的應用前景、技術挑戰及未來發展方向等問題進行了深入探討，現場氣氛熱烈，思想碰撞不斷，研討會取得圓滿成功。