隨著星載軟件在航天器上實(shí)現(xiàn)的功能比重越來越高,星載軟件可靠性和可信性的指標(biāo)要求越來越嚴(yán)格。傳統(tǒng)軟件測(cè)試方法的局限性難以確保萬無一失,形式化方法以其高度數(shù)學(xué)化和嚴(yán)謹(jǐn)性的特點(diǎn),常被應(yīng)用于安全關(guān)鍵軟件的驗(yàn)證。本文針對(duì)星載軟件的高可靠性和充分性驗(yàn)證需求,初步提出了相應(yīng)的形式化驗(yàn)證方案和需求建模實(shí)施過程,對(duì)于后續(xù)整星級(jí)的軟件驗(yàn)證或者其他單機(jī)組件的驗(yàn)證具有一定的參考和借鑒意義。 

【文章來源】：電腦知識(shí)與技術(shù). 2020,16(25)

【文章頁數(shù)】：2 頁

【部分圖文】：

航天星載軟件形式化驗(yàn)證技術(shù)方案

4 星載軟件形式化需求建模實(shí)施過程在航天星載軟件的形式化需求建模過程中，首先需要使用系統(tǒng)化的過程控制引導(dǎo)需求分析者逐步完成從需求文檔到形式化模型轉(zhuǎn)換。在形式化需求模型建立階段，具體流程圖2所示，具體來說有以下三步：

【參考文獻(xiàn)】：
期刊論文
[1]形式化方法概貌[J]. 王戟,詹乃軍,馮新宇,劉志明.  軟件學(xué)報(bào). 2019(01)
[2]形式化驗(yàn)證在軌道交通領(lǐng)域的應(yīng)用[J]. 于文濤.  電腦知識(shí)與技術(shù). 2018(13)

碩士論文
[1]基于模型的軟件需求驗(yàn)證方法研究[D]. 杜澤民.中國航天科技集團(tuán)公司第一研究院 2018
[2]航天型號(hào)軟件的安全性測(cè)試技術(shù)研究[D]. 馬文姣.哈爾濱工業(yè)大學(xué) 2007



本文編號(hào)：3498586