提升可信度的軟體驗證與確認方法

Verification and Validation for Software Trustworthiness

侯玉中(Yu-Chung Hou)

指導教授 ： 范金鳳

元智大學/工程學院/電機與資訊工程研究所/碩士(1998年)

摘要

使用者大眾對資訊軟體系統的信任度是推展資訊化社會的關鍵因素之一。使用者對軟體的信任度，建立在能掌握足夠的「證據」以相信系統之正確性與安全性。而軟體的發展以及其文件之嚴謹性與可理解性，可進一步協助「證據」的獲得、增進證據反映的軟體可信任度。本論文即針對軟體與文件的「嚴謹性」、「可理解性」與「驗證技術」三方面發展整合的驗證方法。
本論文結合OMT物件導向分析的可讀性、以及正規方法SCR表格精密嚴謹的特性，產生集二者之長的文件格式，並且在其上發展以證據為基礎的軟體驗證與確認技術，以期提升軟體的可信任度。最後完成一個實例，以證明方法確實可行。

關鍵字

正規方法 ； 物件導向分析 ； 以證據為基礎 ； 驗證與確認方法

並列摘要

The public’s of trust in software systems is one of the essential factors for the success of information society. User’s trust in software relies on their acquisition of “evidence” that the system is correct and safe. The “precision” and “understandability” of software development process and related documents may facilitate the search of evidence and improve the trustworthiness of software. This thesis aims to develop an integrated verification method at these aspects.
This thesis combines the readability of the object-oriented analysis method OMT and the preciseness of formal method SCR to produce a new software requirement/specification format. On these documents, we then develop the verification technique based on Evidence-Based Verification and Validation to enhance the trustworthiness of software. A case study has been completed to demonstrate the feasibility of the proposed approach.

並列關鍵字

formal method ； OOA ； evidence-based ； V & V

參考文獻

[3] L. M. Barroca, and J. A. McDermid, “Formal Methods: Use And Relevance for the Development of Safety-Critical Systems,” The Computer Journal, Vol.35, No.6, 1992, pp.579-599.

[4] C. Heitmeyer, B. Labaw, and D. Kiskis. “Consistency Checking of SCR-style Requirements Specifications,” In Proc. 1995 Int’l Symposium on Requirements Engg., York, England, Mar. 1995.

[5] C. Heitmeyer, A. Bull, C. Gasarch, and B. Labaw, “A Toolset for Specifing and Analyzing Requirements”, IEEE, 1995, pp.109-122.

[6] C. Heitmeyer, R. Jeffords, and B. Labaw, “Automated Consistency Checking of Requirements Specifications,” ACM Trans. on Software Engg. and Methodology, (5)3, July 1996, pp.231-261.

[9] R. Bharadwaj and C. Heitmeyer, “Applying the SCR Requirements Method to a Simple Autopilot,” Proc. of Fourth NASA Lanngley Formal Methods Workshop, Sep. 1997.