龔業(yè)等

隨著社會不斷的發(fā)展，我國信息技術(shù)水平逐漸提高，軟件成為了系信息技術(shù)中重要組成部分?，F(xiàn)階段，人們對軟件的質(zhì)量、安全性、穩(wěn)定性、可靠性等有著較高的要求，高可信軟件工程技術(shù)可以有效的滿足人們的需求，保證軟件在運(yùn)行時的質(zhì)量與效率?；诖?，本文對高可信軟件工程技術(shù)進(jìn)行了簡單的研究。

【關(guān)鍵詞】高可軟件 工程技術(shù)

隨著社會不斷的發(fā)展，計算機(jī)技術(shù)在各行業(yè)中得到了廣泛的應(yīng)用，其中的軟件系統(tǒng)也成為了國民經(jīng)濟(jì)發(fā)展的重要組成部分。軟件的出現(xiàn)改變了人們傳統(tǒng)的生活方式，將人們?nèi)粘?chuàng)新，使軟件成為人們?nèi)粘Ｉ畈豢扇鄙俚囊徊糠?。另外，軟件的出現(xiàn)也成為一個全新的信息設(shè)施，在網(wǎng)上銀行、電子商務(wù)等領(lǐng)域中得到了廣泛的應(yīng)用，如果沒有軟件那么這些領(lǐng)域就不會再出現(xiàn)，由此可見，軟件對于社會發(fā)展的重要性。但是一些軟件在實際運(yùn)行過程中，其質(zhì)量、安全性、可靠性等方面還存在著一定不足，如何保證軟件在設(shè)計過程中具有較高的可信性質(zhì)已經(jīng)成為了軟件在發(fā)展過程中所研究的重要話題之一。

1 高可信軟件概述

傳統(tǒng)的技術(shù)所生產(chǎn)出來的軟件主要通過模型的建立、演算、測試、驗證形成，從而保證所生產(chǎn)出來的產(chǎn)品具有一定的期望性質(zhì)。隨著社會不斷的發(fā)展，傳統(tǒng)生產(chǎn)技術(shù)已經(jīng)跟不上社會發(fā)展的腳步，只有將其不斷的創(chuàng)新、完善才能保證所生產(chǎn)出來的產(chǎn)品可以在這個競爭激烈的社會中站穩(wěn)腳步。而高可信軟件在生產(chǎn)過程中主要通過后置斷言的順序形將軟件的整體理論進(jìn)行推理，并將其以順序計算的形式展現(xiàn)出來，只有這樣才能將現(xiàn)有的程序模型以輸出對形式映射出來，從而形成一個全新相應(yīng)模式，并保證軟件具有較高的可信性、安全性、穩(wěn)定性。

2 高可信軟件特點

要想保證軟件系統(tǒng)在設(shè)計過程中具有較高的可信形式就需要滿足一些關(guān)鍵性質(zhì)的需求，只有這樣才能保證所設(shè)計出來的軟件系統(tǒng)具有較高的可信形式。如果在設(shè)計過程中沒有滿足關(guān)鍵性質(zhì)的需求就會降低整個軟件系統(tǒng)的安全性與可靠性，從而導(dǎo)致軟件系統(tǒng)不能正常使用。

要想保證軟件系統(tǒng)在設(shè)計過程中具有較高的可信性質(zhì)就需要滿足以下幾點關(guān)鍵性質(zhì)特點，如圖1所示。

2.1 可靠性

在對軟件系統(tǒng)設(shè)計過程中要為其制定一項科學(xué)合理的設(shè)計方案，只有這樣才能保證信息系統(tǒng)可以指定的時間內(nèi)完成，保證軟件系統(tǒng)的可靠性。

2.2 安全性

在軟件系統(tǒng)設(shè)計過程中將考慮到軟件在運(yùn)行過程中所發(fā)生的安全故障，不能夠為其制定有效的防護(hù)措施，只有這樣才能保證軟件在運(yùn)行時候不會發(fā)生安全故障。

2.3 保密性

保密性的高可信軟件系統(tǒng)中重要組成部分，做好軟件的保密工作可以有效的保證數(shù)據(jù)在傳輸、存儲過程中的安全。

2.4 生存性

如果軟件在運(yùn)行過程中受到外界攻擊，沒有完整的生存性就會導(dǎo)致軟件不能正常使用。因此在對軟件系統(tǒng)設(shè)計過程中要做好生存性對設(shè)計工作，就算出現(xiàn)問題時軟件也可以自行修復(fù)，保證軟件可以正常運(yùn)行。

2.5 實時性

實時性主要指軟件在運(yùn)行過程中具有良的反應(yīng)、輸出、提交能力，從而保證軟件在運(yùn)行過程中的穩(wěn)定性。

3 高可信軟件工程技術(shù)現(xiàn)狀

3.1 軟件形式化法

形式化法是軟件系統(tǒng)設(shè)計中重要組成部分，同時也是一種嚴(yán)格的軟件開發(fā)系統(tǒng)。因此，在軟件系統(tǒng)開發(fā)過程中要保證其具有先進(jìn)的思想、方法、技術(shù)只有這樣才能促進(jìn)軟件系統(tǒng)快速發(fā)展。形式化方法可以有效的對整個計算機(jī)系統(tǒng)進(jìn)行推理測試，并對一些形式化的規(guī)約技術(shù)進(jìn)行驗證，找出其中的不足，并為其制定有效的解決對策。合理應(yīng)用形式化方法可以有效的提高軟件的質(zhì)量與效率，這對于提高可信軟件的安全性來說也有著非常大的幫助。

3.2 軟件測試、設(shè)計技術(shù)

軟件的可信性對于軟件系來說有著非常重要的關(guān)系，因此，在軟件系統(tǒng)實際測試過程中要做好軟件系統(tǒng)的測試與設(shè)計工作，只有這樣才能保證軟件系統(tǒng)具有較高的安全性。而軟件系統(tǒng)的測試工作主要通過對軟件的判斷形式的，可以將軟件中的性質(zhì)展現(xiàn)出來，對于軟件系統(tǒng)的開發(fā)工作來說也是非常重要的一部分。對于軟件系統(tǒng)的工程設(shè)計來說，我國所使用的設(shè)計工作主要通過軟件高可信手段進(jìn)行處理，從而滿足軟件系統(tǒng)在發(fā)展時的需求，保證軟件系統(tǒng)具有較高的安全性、可靠性、

隨著社會不斷的發(fā)展，軟件系統(tǒng)的設(shè)計工作應(yīng)取得了較大的成效。而形式化方法對于軟件系統(tǒng)的設(shè)計工作來說有著至關(guān)重要的關(guān)系。要想保證軟件系統(tǒng)的質(zhì)量就需要對軟件系統(tǒng)的程序理論進(jìn)行深入研究，并在其中制定出全新的可信性質(zhì)的設(shè)計方法與技術(shù)。而軟件開發(fā)工作是一項極為復(fù)雜的過程，因此，在對軟件時要從根本上提高軟件的質(zhì)量與效率，只有這樣才能保證軟件系統(tǒng)在運(yùn)行時的安全性。

4 總結(jié)

高可信軟件技術(shù)對于社會的發(fā)展有著非常重要的關(guān)系，只有人們認(rèn)識到高可信軟工程技術(shù)的價值才能做好其設(shè)計工作，并其中的真正價值發(fā)揮出來，從而保證軟件在運(yùn)行時的安全性、穩(wěn)定性、可靠性。本文對高可信軟件工程技術(shù)進(jìn)行了簡單的分析，文中還存在著一定的不足，希望我國專業(yè)技術(shù)人員加強(qiáng)對其的研究。

參考文獻(xiàn)

[1]楊芙清，梅宏，呂建，金芝.淺論軟件技術(shù)發(fā)展[J].電子學(xué)報，2014（09）.

[2]林惠民，張文輝.模型檢測：理論、方法與應(yīng)用[J].電子學(xué)報，2014（11）.

[3]George C Necula，Peter Lee.Safe kernel extensions without run-timechecking[A].2nd Symposium onOperating Systems Design and Imple-mentation （OSDI'96）[M].Seattl，WA，October，2003.229-243.

[4]SumantKowshik，DinakarDhurjati， VikramAdve.Ensuring code safetywithout runtime checks for real -time control systems[A].Proc IntConfonCompilers，ArchitectureandSynthesis for EmbeddedSystems（CAS-ES02）[C].Grenoble， France，Oct，2002：288-297.

作者單位

同濟(jì)大學(xué)軟件學(xué)院 上海市 201804