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