11月27日，2022年CCF中國軟件大會“形式化方法工業(yè)應用前沿”技術分論壇于線上順利召開。本次活動由CCF形式化方法專業(yè)委員會主辦，華東師范大學、國防科技大學承辦，上海工業(yè)控制安全創(chuàng)新科技有限公司、科大國創(chuàng)軟件股份有限公司、安徽中科國創(chuàng)高可信軟件有限公司協辦。活動邀請工業(yè)界與學術界的頂尖專家，聚焦工業(yè)領域中形式化方法的應用探索，共同討論形式化方法在工業(yè)領域應用的最佳實踐以及發(fā)展趨勢。活動于騰訊會議等多個平臺同步直播，受到業(yè)界同行及高校師生的熱烈響應，超1,000人次實時在線觀看。會上，同步舉辦中科國創(chuàng)高可信與上海控安新品聯合發(fā)布會。

活動由華東師范大學軟件工程學院執(zhí)行院長、教授、博士生導師、上海控安總經理蒲戈光，國防科技大學計算機學院教授、博士生導師董威擔任主席。蒲戈光作開場致辭，介紹本次論壇的背景與意義。他表示形式化方法是保障軟硬件可靠性與正確性的重要手段，目前已覆蓋芯片驗證、操作系統驗證、程序分析等工業(yè)應用領域。本次活動希望通過工業(yè)界與學術界的交流，共同促進形式化方法領域產業(yè)與學術共同體的發(fā)展。董威向蒞臨參會的各位嘉賓表示歡迎，并擔任本次論壇主持。

國防科技大學計算機學院 董威

報告分享

隨后，來自科大國創(chuàng)高可信公司、華東師范大學、華為、芯華章科技股份有限公司等優(yōu)秀企業(yè)高校的多位專家學者作主題報告演講。

科大國創(chuàng)高可信公司，研發(fā)總監(jiān)，李兆鵬，以“形式化方法在工業(yè)控制領域的研究與實踐”為主題，結合自身實戰(zhàn)經驗，著重討論當下形式化方法的程序驗證實踐與靜態(tài)分析實踐，并展望工業(yè)領域中形式化方法的發(fā)展與挑戰(zhàn)。

科大國創(chuàng)高可信公司 李兆鵬

華東師范大學軟件工程學院，教授、博士生導師，李建文，圍繞“形式化驗證技術及其EDA應用案例”，介紹當前主流硬件形式化驗證技術的基本原理、發(fā)展進程和現有不足，并通過實踐案例闡述理論研究與實際應用場景相結合的具體途徑。

華東師范大學軟件工程學院 李建文

華為操作系統內核實驗室，工程師，李屹，就“操作系統開發(fā)中的形式化驗證：挑戰(zhàn)與思考”進行演講，結合自身在操作系統內核形式化驗證方面的實踐經驗，分享在形式化驗證實踐過程中所遇到的挑戰(zhàn)，以及相應的解決措施與思考。

華為操作系統內核實驗室 李屹

華為公司可信系統工程實驗室，技術專家，梁智章，分享主題“安全攸關領域的形式化方法試點和探索”，介紹形式化方法在安全攸關領域中的落地應用，并分享華為可信系統工程實驗室對形式化方法的應用和探索。

華為公司可信系統工程實驗室 梁智章

芯華章科技動態(tài)仿真與形式驗證部，研發(fā)總監(jiān)，劉軍，圍繞主題“形式驗證覆蓋率分析加速芯片驗證收斂”，以芯片驗證領域中的形式化方法發(fā)展進程為切入點，分享形式驗證的具體實踐與思考。

產品發(fā)布

活動最后，中科國創(chuàng)高可信與上?？匕猜摵习l(fā)布形式化軟件工具鏈——“科創(chuàng)星云驗證器（企業(yè)版）”& “SmartRocket Modeler可視化建模開發(fā)工具（beta版）”。中科國創(chuàng)高可信市場總監(jiān)李超鈺、咨詢總監(jiān)周洋，上?？匕伯a品總監(jiān)包丹珠，以及線上各位嘉賓觀眾共同見證產品發(fā)布。李超鈺表示，本次聯合發(fā)布的形式化軟件工具鏈將形式化技術應用于實踐，推動了形式化方法的深化與創(chuàng)新，為關鍵行業(yè)領域的數智化產品進一步提供了保障與支撐，也為中國乃至全球的工業(yè)軟件安全保障提供了多種可能性。

產品發(fā)布

中科國創(chuàng)高可信 科創(chuàng)星云驗證器（企業(yè)版），采用自主設計的安全C規(guī)范語言作為規(guī)約語言，對程序的行為進行形式化描述。基于Hoare邏輯，采用最強后條件的演繹推理技術，將程序滿足其形式規(guī)約的證明問題轉化為一組數學命題的證明，并實現程序驗證的自動化?？苿?chuàng)星云驗證器主要用于關鍵核心代碼的驗證，比如操作系統內核、數據庫引擎、關鍵的嵌入式軟件等，為航空航天、汽車電子、能源核電、軌道交通等安全攸關領域的高可信軟件開發(fā)提供安全保障。

科創(chuàng)星云驗證器（企業(yè)版）

官網：www.ustchcs.com

郵箱：info@ustchcs.com

電話：0551-65396781

上?？匕?SmartRocket Modeler可視化建模開發(fā)工具，是一款國產自主可控的可視化建模開發(fā)工具。該工具支持嵌入式軟件模型的設計與開發(fā)，能夠從系統需求出發(fā)，為用戶提供基于Lustre模型語言的圖形化建模、模型靜態(tài)檢查、模型仿真與調試、模型在環(huán)測試、C代碼自動生成等豐富便捷的功能。同時工具也支持全系列國產操作系統，為國內高端制造領域的嵌入式軟件研制提供支撐平臺，為逐步擺脫對國外同類軟件的依賴提供有效解決方案。

SmartRocket Modeler

可視化建模開發(fā)工具（beta版）

官網：m.zhizhu2014.com

郵箱：Marketing@ticpsh.com

電話：021-62655886（工作日09:00-18:00）

至此，2022 CCF形式化方法工業(yè)應用前沿分論壇圓滿完成?；顒悠陂g，專家學者通過視頻分享精彩觀點，并與線上與會的嘉賓積極互動，從工業(yè)界與學術界等維度熱烈探討形式化方法的具體落地實踐。未來，上?？匕惨矊⒗^續(xù)深化拓展產業(yè)與學術需求交叉，加快推動科研成果轉化，促進形式化方法的理論研究、工具成果和行業(yè)實踐的融合發(fā)展。

閱讀原文