賀 飛, 張立軍

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

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

3(信息系統(tǒng)安全教育部重點(diǎn)實(shí)驗(yàn)室,北京 100084)

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

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

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

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

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

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

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

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

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

論文“一種同步語(yǔ)言多線程代碼自動(dòng)生成工具”提出了一種從同步語(yǔ)言SIGNAL到多線程代碼的自動(dòng)生成工具,并在多核處理器上進(jìn)行了實(shí)驗(yàn)驗(yàn)證.

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

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

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

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