高可信軟件工程技術的特點和現狀

龔業等

隨著社會不斷的發展，我國信息技術水平逐漸提高，軟件成為了系信息技術中重要組成部分。現階段，人們對軟件的質量、安全性、穩定性、可靠性等有著較高的要求，高可信軟件工程技術可以有效的滿足人們的需求，保證軟件在運行時的質量與效率。基于此，本文對高可信軟件工程技術進行了簡單的研究。

【關鍵詞】高可軟件 工程技術

隨著社會不斷的發展，計算機技術在各行業中得到了廣泛的應用，其中的軟件系統也成為了國民經濟發展的重要組成部分。軟件的出現改變了人們傳統的生活方式，將人們日常創新，使軟件成為人們日常生活不可缺少的一部分。另外，軟件的出現也成為一個全新的信息設施，在網上銀行、電子商務等領域中得到了廣泛的應用，如果沒有軟件那么這些領域就不會再出現，由此可見，軟件對于社會發展的重要性。但是一些軟件在實際運行過程中，其質量、安全性、可靠性等方面還存在著一定不足，如何保證軟件在設計過程中具有較高的可信性質已經成為了軟件在發展過程中所研究的重要話題之一。

1 高可信軟件概述

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

2 高可信軟件特點

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

要想保證軟件系統在設計過程中具有較高的可信性質就需要滿足以下幾點關鍵性質特點，如圖1所示。

2.1 可靠性

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

2.2 安全性

在軟件系統設計過程中將考慮到軟件在運行過程中所發生的安全故障，不能夠為其制定有效的防護措施，只有這樣才能保證軟件在運行時候不會發生安全故障。

2.3 保密性

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

2.4 生存性

如果軟件在運行過程中受到外界攻擊，沒有完整的生存性就會導致軟件不能正常使用。因此在對軟件系統設計過程中要做好生存性對設計工作，就算出現問題時軟件也可以自行修復，保證軟件可以正常運行。

2.5 實時性

實時性主要指軟件在運行過程中具有良的反應、輸出、提交能力，從而保證軟件在運行過程中的穩定性。

3 高可信軟件工程技術現狀

3.1 軟件形式化法

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

3.2 軟件測試、設計技術

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

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

4 總結

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

參考文獻

[1]楊芙清，梅宏，呂建，金芝.淺論軟件技術發展[J].電子學報，2014（09）.

[2]林惠民，張文輝.模型檢測：理論、方法與應用[J].電子學報，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.

作者單位

同濟大學軟件學院 上海市 201804