《基於構件的高可信系統形式驗證研究》是依託中國人民解放軍國防科技大學，由董威擔任項目負責人的青年科學基金項目。
基本介紹
- 中文名：基於構件的高可信系統形式驗證研究
- 項目類別：青年科學基金項目
- 項目負責人：董威
- 依託單位：中國人民解放軍國防科技大學
- 負責人職稱：教授
- 批准號：60303013
- 研究期限：2004-01-01 至 2006-12-31
- 申請代碼：F0202
- 支持經費：24（萬元）
中文摘要
基於構件的軟體開發方法已套用於高可信軟體系統的開發。研究基於構件的安全攸關係統的形式驗證方法，對加強高可信系統的安全可靠性、促進構件技術的套用和發展具有重要的科學意義和套用價值。本項目的研究內容包括：以載人航天、武器控制等安全攸關領域的典型案例為背景，研究構件技術在高可信軟體系統開發中的特點和軟體體系結構，建立能準確刻畫高可信構件系統並發、分布、實時、容錯等特徵的形式模型和集成語義；建立描述高可信構件系統關鍵性質的形式規約技術；針對基於構件的高可信系統的典型軟體體系結構模式和性質模版研究形式驗證框架和高效模型檢驗算法；根據構件系統的分布、並發和層次等結構特點研究組合驗證技術，把模型檢驗和演繹推理結合起來驗證複雜系統；面向性質研究抽象、切片等緩解系統狀態爆炸的方法；並基於主流軟體工程環境建立形式驗證工具。
