《面向性質的可信軟體建模與時序性質驗證及支持工具》是依託北京航空航天大學，由李舟軍擔任項目負責人的重大研究計畫。
基本介紹
- 中文名：面向性質的可信軟體建模與時序性質驗證及支持工具
- 依託單位：北京航空航天大學
- 項目負責人：李舟軍
- 項目類別：重大研究計畫
- 批准號：90718017
- 申請代碼：F0203
- 負責人職稱：教授
- 研究期限：2008-01-01 至 2010-12-01
- 支持經費：50（萬元）
項目摘要
面向性質的可信軟體建模與時序性質驗證及支持工具具有重要的研究價值。本課題以抽象解釋理論中的逼近計算作為抽象複雜計算的理論工具，結合軟體測試和軟體驗證方法中的路徑條件、偏序消減、符號化執行、約束求解、惰性計算等多種技術，以驗證可信軟體的時序性質作為主要研究內容，需要解決的理論問題有：可信軟體面向性質的高精度程式切片方法，可信軟體面向驗證性質的抽象遷移模型構造，基於反例制導的抽象精化疊代驗證框架的可信
