https://scholars.lib.ntu.edu.tw/handle/123456789/105196
標題: | 元件合成軟體之形式化驗證初探 | 其他標題: | Toward Formal Verification of Component-Based Software | 作者: | 蔡益坤 | 關鍵字: | 假設∕保證;元件合成軟體;組合 式驗證;形式化方法;模型檢驗器;模組化 驗證;證明助理;軟體元件;規格;時間邏 輯;驗證;Assumption-Guarantee;Component-Based Software;Compositional Verification;Formal Methods;Model Checkers;Modular Verification;Proof Assistants;Software Components;Specification;Temporal Logic;Verification | 公開日期: | 2004 | 出版社: | 臺北市:國立臺灣大學資訊管理學系暨研究所 | 摘要: | 以元件為基礎之設計已成為軟體開發 的主流方法之一。本研究旨在探討元件合成 軟體正確性規格與驗證的問題。由於構成這 類軟體的各元件通常是由不同團體獨立開發 完成,元件設計者需要一種描述元件而不揭 露其程式碼的方法,也就是一種可描述元件 做什麼而不必交代它是如何做的方法。而元 件合成軟體開發者需要一套驗證方法,在給 定他個人所寫的程式碼以及所引用元件的規 格後,檢驗他的合成系統確實正確無誤。 過去我們已發展出一套組合式規格與 驗證的架構,本研究嘗試將這套架構運用在 前述元件合成軟體規格與驗證的工作。我們 特別針對部份元件僅有規格而無程式碼的情 形,闡述這套架構如何使用。我們同時也探 討如何以自動化驗證工具來協助這些驗證工 作的進行。 Component-based design has become a prominent approach to software development.In this project we consider the task of formally specifying and verifying behavioral correctness of software built from independently developed components.The task requires a way for the component designer to describe his component without revealing the code,i.e.,to specify what the component does but not how it gets things done.It also requires a way for the component-based software developer to verify his system,given the source code of the part that he coded and the specifications of the components that he used. We adapt a compositional framework that we have developed earlier for carrying out the aforementioned specification and verification tasks. In particular,we demonstrate how the framework may be used in a typical case where some components of a system can be reasoned only with their behavioral specification but not their code.We also investigate how the verification tasks can be facilitated by automated tools. |
URI: | http://ntur.lib.ntu.edu.tw//handle/246246/18840 | 其他識別: | 922213E002061 | Rights: | 國立臺灣大學資訊管理學系暨研究所 |
顯示於: | 資訊管理學系 |
檔案 | 描述 | 大小 | 格式 | |
---|---|---|---|---|
922213E002061.pdf | 293.08 kB | Adobe PDF | 檢視/開啟 |
在 IR 系統中的文件,除了特別指名其著作權條款之外,均受到著作權保護,並且保留所有的權利。