Modeling and Hybrid Verification of High-Assurance Properties for Real Time Software Systems

瀏覽統計 Email 通知 RSS Feed

簡歷

基本資料

Project title

Code/計畫編號

NSC93-2213-E033-031

Translated Name/計畫中文名

高保證性即時軟體系統的軟體模型和混合性正規驗證法

Project Coordinator/計畫主持人

Yee-Jsong Juan

Funding Organization/主管機關

National Science and Technology Council

Department/Unit

Department of Computer Science and Engineering

Website

https://www.grb.gov.tw/search/planDetail?id=1016764

Year

2004

Start date/計畫起

01-08-2004

Expected Completion/計畫迄

31-07-2005

Bugetid/研究經費

415千元

ResearchField/研究領域

資訊科學--軟體

即時軟體系統的正確包含反應時間以及功能的正確。幾年前，即時軟體系統主要應用於軍方和太空探險。可是今日軟體幾乎都需要即時性的需求。今日大部分的軟體是軟性即時，可是有硬性即時的限制。網際網路的快速成長創造了建構大型軟體系統的機會。一個大型軟體系統可以包含超過兩百萬電腦並使用超過兩十萬CPU 計算時間[7]。大型即時軟體系統的建構已是可達到的。今日自動化正規驗證法已成功地應用在驗證實際的即時軟體系統。可惜的是正規驗證法的分析能力遠遠落後於軟體系統大小的增長。更糟的是即時軟體系統的正規驗證是更複雜，因為即時軟體系統的正確性包含功能性以及時間性的正確。一個即時程序狀態的後繼程序狀態可能是多樣化並急遽的增加。這個事實增加驗證的複雜並妨礙高效率分析技術的發展。因此大型即時軟體系統極度需求新型的高效率的正規驗證法。為了解決這個問題，此研究計劃將發展新的正規驗證法應用於大型即時軟體系統。我們將專注於開發新的基礎理論和混合性的正規驗證法。根據我們前幾年的研究成果，我們預計此研究計劃將有深遠的貢獻於即時軟體系統的正規驗證。我們新的技術將增強即時軟體系統的生產和可靠性，並減少軟體開發的時間。此研究計劃所發展出的即時軟體驗證工具將對正規驗證法的實際運用有重要的貢獻。

Keyword(s)

即時軟體系統
軟性即時
硬性即時
正規驗證
高效率分析
時間的限制
程序狀態的劇增

DSpace CRIS

Modeling and Hybrid Verification of High-Assurance Properties for Real Time Software Systems

基本資料

Description