2003-08-012024-05-18https://scholars.lib.ntu.edu.tw/handle/123456789/709908摘要：在本研究中我們探討元件合成軟體正確性驗證的問題。構成這類軟體中各模組的元件通常是由不同團體獨立開發完成，其程式碼原則上不會公開。可以預見的，這促使元件設計者需要一種描述元件而不揭露程式碼的方法，也就是一種可描述元件做些什麼事而不必交代它是怎麼做到的方法。該描述內容即元件之規格必須充分詳細，以使其他系統能正確地使用該元件。這裡所謂正確地使用意指，在以前項元件做為系統之一模組下，該系統整體運作正常無誤。而這進一步促使元件合成軟體開發者需要一套驗證方法，在給定他個人寫的程式碼以及所引用元件的規格後，檢驗他的合成系統確實正確無誤。 過去我們使用線性時間邏輯(Linear-Time Temporal Logic)所發展出的一套組合式驗證架構，似乎適用於前述的驗證工作。該架構包含一種適於描述系統模組的假設∕保證式規格(assumption-guarantee specifications)的撰寫方式，以及組合假設∕保證式規格的驗證法則。本研究的主要目的之一便是在測試我們的組合式驗證架構在元件合成軟體驗證上的應用。為使研究成果更具實務價值，我們將努力提高驗證過程自動化的程度。其中，我們將嘗試改良並<br> Abstract: In this research we consider the task of formally verifying software built from independently developed components, whose source code may not be disclosed. Conceivably, this 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. The specification should be sufficiently precise so that some other system can make a correct usage of the component in that, with the component as a part, the system as a whole behaves properly. This in turn 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 have developed a compositional framework in linear-time temporal logic which appears to be applicable to the aforementioned verification task. The framework consists of a formulation of assumption-guarantee specifications that is suitable for specifying the modules of a system and composition rules for composing such specifications. One primary goal of this research is to test using our compositional framework in verifying component-based software. To make our work more practically useful, we shall seek a high degree of automation of the verification process. Specifically, we shall attempt to adapt the so-called bounded model checking to carry out the proof obligations that arise from applying our composition rules. Note: This research represents our initial investigation on the concerned subject and is of foundational nature. We shall assume a minimal set of programming language features and treat software mainly in the semantic level, modeling them as state-transition systems.假設∕保證自動驗證元件合成軟體組合式驗證正確性形式化方法模型檢驗模組化驗證軟體元件規格時間邏輯驗證Assumption-GuaranteeAutomated VerificationComponent-Based SoftwareCompositional VerificationCorrectnessFormal MethodsModel CheckingModular VerificationSoftware ComponentsSpecificationTemporal LogicVerification