摘要：時(shí)段演算是描述和推導(dǎo)嵌入式實(shí)時(shí)系統(tǒng)和混成系統(tǒng)性質(zhì)的一種區(qū)間時(shí)態(tài)邏輯。擴(kuò)展線性時(shí)段不變式是時(shí)段演算的重要子集。針對(duì)實(shí)時(shí)自動(dòng)機(jī),提出一種連續(xù)時(shí)間語(yǔ)義下擴(kuò)展線性時(shí)段不變式的有界模型檢驗(yàn)方法。該方法將擴(kuò)展線性時(shí)段不變式的有界模型檢驗(yàn)問(wèn)題轉(zhuǎn)化為量詞線性算術(shù)公式的正確性問(wèn)題,從而可以采用量詞消去技術(shù)進(jìn)行求解。首先,運(yùn)用符號(hào)化的思想,在實(shí)時(shí)自動(dòng)機(jī)上利用深度優(yōu)先搜索找到所有滿足觀測(cè)時(shí)長(zhǎng)約束的符號(hào)化路徑片段;然后,將每條符號(hào)化路徑片段轉(zhuǎn)化為一個(gè)量詞線性算術(shù)公式;最后,利用量詞消去工具求解。與已有工作相比,基于實(shí)時(shí)自動(dòng)機(jī)設(shè)計(jì)了驗(yàn)證算法。另外,降低了驗(yàn)證復(fù)雜度,并且加速了驗(yàn)證過(guò)程的實(shí)際速度。