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

賀 飛, 張立軍

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

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

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

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

5(廣州智能軟件產(chǎn)業(yè)研究院,廣東 廣州 511458)

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

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

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

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

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

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

論文“面向?qū)崟r數(shù)據(jù)的CPS一體化建模方法”針對CPS在復(fù)雜環(huán)境中的安全性和可靠性問題,提出了一種面向?qū)崟r數(shù)據(jù)的一體化建模方法,并針對移動機器人進行了案例分析.

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

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

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

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

本專題面向形式化方法的研究人員和工程人員,內(nèi)容涵蓋系統(tǒng)軟件、軟件工程、嵌入式系統(tǒng)等領(lǐng)域,反映了我國學(xué)者在形式化驗證理論、方法、工具和應(yīng)用等方面的高水平研究成果.感謝《軟件學(xué)報》編委會、CCF形式化方法專委會對專題工作的指導(dǎo)和幫助,感謝專題全體評審專家及時、耐心、細(xì)致的評審工作,感謝踴躍投稿的所有作者.希望本專題能夠?qū)π问交椒ǖ目蒲泄ぷ饔兴龠M.