基于實時自動機的連續時段演算的驗證
作者：安杰; 張苗苗 同濟大學軟件學院; 上海201804
摘要：時段演算是描述和推導嵌入式實時系統和混成系統性質的一種區間時態邏輯。擴展線性時段不變式是時段演算的重要子集。針對實時自動機,提出一種連續時間語義下擴展線性時段不變式的有界模型檢驗方法。該方法將擴展線性時段不變式的有界模型檢驗問題轉化為量詞線性算術公式的正確性問題,從而可以采用量詞消去技術進行求解。首先,運用符號化的思想,在實時自動機上利用深度優先搜索找到所有滿足觀測時長約束的符號化路徑片段;然后,將每條符號化路徑片段轉化為一個量詞線性算術公式;最后,利用量詞消去工具求解。與已有工作相比,基于實時自動機設計了驗證算法。另外,降低了驗證復雜度,并且加速了驗證過程的實際速度。
注：因版權方要求，不能公開全文，如需全文，請咨詢雜志社。
軟件學報雜志
軟件學報雜志， 月刊，本刊重視學術導向，堅持科學性、學術性、先進性、創新性，刊載內容涉及的欄目：理論計算機科學、系統軟件與軟件工程、模式識別與人工智能、數據庫技術、計算機網絡與信息安全、計算機體系結構等。于1990年經新聞總署批準的正規刊物。
- 北大期刊
- CSCD期刊
- 統計源期刊
- 1-3個月審核
