軟件形式化驗證專題前言*

賀 飛, 張立軍

1(清華大學 軟件學院,北京 100084)

2(北京信息科學與技術國家研究中心,北京 100084)

3(信息系統安全教育部重點實驗室,北京 100084)

4(中國科學院 軟件研究所,北京 100190)

5(廣州智能軟件產業研究院,廣東 廣州 511458)

形式化方法是建立在邏輯演算、形式語言、自動機理論、程序語義、類型系統等理論基礎之上,對計算系統進行描述和分析的一系列符號與技術的集合.形式化方法可指導軟/硬件系統的規約、設計和驗證,是改善和確保計算系統質量的重要方法.歷史上,形式化方法在硬件和協議驗證方面取得巨大成功.近年來,隨著相關技術的發展,形式化方法已在越來越多的軟件系統中得到應用,并取得顯著成效.為記錄中國學者在形式化驗證理論、方法、工具和應用等方面的最新研究成果,特設立此專題.

本專題采取定向邀請和自由投稿相結合的方式,共收到22篇投稿,其中20篇通過了形式審查.特約編輯邀請了40余位領域專家參與審稿,每篇稿件至少邀請2位專家進行評審,每篇稿件都經過兩輪審稿.共計11篇稿件通過第1輪評審,并在CCF形式化方法專委會年度會議上進行了報告.經過第2輪終審,最終有9篇論文入選本專題.其中,

論文“基于 SVM的多項式循環程序秩函數生成”研究程序終止性問題,將秩函數計算問題歸結為二分類問題,并提出了利用支持向量機(SVM)計算程序秩函數的方法.

論文“高階類型化軟件體系結構建模和驗證及案例”提出了一種高階類型化的軟件體系結構建模語言和相應的體系結構建模驗證方法,支持主流Web應用體系結構的建模和驗證.

論文“非交互式Petri網可覆蓋性驗證的高效實現”研究非交互式Petri網可覆蓋性驗證問題,在理論上給出了該問題的完備性判定方法,并給出了工具實現.

論文“基于實時自動機的連續時段演算的驗證”研究在標準連續時間語義下基于實時自動機的擴展線性時段不變式的有界模型檢驗問題,證明了該問題是可判定的,并且給出模型檢驗算法.

論文“面向實時數據的CPS一體化建模方法”針對CPS在復雜環境中的安全性和可靠性問題,提出了一種面向實時數據的一體化建模方法,并針對移動機器人進行了案例分析.

論文“一種同步語言多線程代碼自動生成工具”提出了一種從同步語言SIGNAL到多線程代碼的自動生成工具,并在多核處理器上進行了實驗驗證.

論文“同步數據流語言可信編譯器Vélus與L2C的比較”從源語言特性、編譯器結構、翻譯正確性驗證等多個角度對同步數據流語言編譯器Vélus和L2C進行了較為深入的分析與比較,能夠為編譯器可信構造研究提供參考.

論文“具有多傳感器的CPS系統的攻擊檢測”研究存在瞬態故障的CPS中傳感器的攻擊檢測問題,設計了一種基于融合間隔和歷史測量的傳感器攻擊檢測方法.

論文“有關時間自動機重置的若干問題的計算復雜性”研究完全確定時間自動機、部分規約的確定時間自動機以及非確定時間自動機的計算復雜性問題,并給出了有關復雜度估計的若干理論結果.

本專題面向形式化方法的研究人員和工程人員,內容涵蓋系統軟件、軟件工程、嵌入式系統等領域,反映了我國學者在形式化驗證理論、方法、工具和應用等方面的高水平研究成果.感謝《軟件學報》編委會、CCF形式化方法專委會對專題工作的指導和幫助,感謝專題全體評審專家及時、耐心、細致的評審工作,感謝踴躍投稿的所有作者.希望本專題能夠對形式化方法的科研工作有所促進.