對(duì)PTL和MSVL的實(shí)時(shí)擴(kuò)展.pdf

1、實(shí)時(shí)系統(tǒng)經(jīng)常被用在飛機(jī)、軍事以及交通控制等安全攸關(guān)的領(lǐng)域，因此保證其正確性和安全性至關(guān)重要。建模、仿真及驗(yàn)證語(yǔ)言（MSVL）是一種基于投影時(shí)序邏輯（PTL）的時(shí)序邏輯程序設(shè)計(jì)語(yǔ)言，它可用于對(duì)計(jì)算機(jī)軟、硬件系統(tǒng)進(jìn)行建模、仿真和驗(yàn)證。但由于PTL和MSVL中缺乏對(duì)量化時(shí)間的描述能力，因此，很多實(shí)時(shí)系統(tǒng)及其性質(zhì)無(wú)法被描述。
　　本文通過(guò)對(duì)PTL和MSVL的實(shí)時(shí)擴(kuò)展，得到的實(shí)時(shí)建模、仿真及驗(yàn)證語(yǔ)言（TMSVL）可以對(duì)實(shí)時(shí)系統(tǒng)進(jìn)行建模、仿真

2、和驗(yàn)證。首先，介紹了PTL和MSVL的語(yǔ)法和語(yǔ)義及其相關(guān)理論；然后，通過(guò)定義時(shí)間約束區(qū)間將PTL擴(kuò)展為可以描述量化時(shí)間約束的實(shí)時(shí)投影時(shí)序邏輯（TPTL），形式化定義了TMSVL的語(yǔ)句和程序，并給出了TMSVL的操作語(yǔ)義，還利用TMSVL基本語(yǔ)句定義了實(shí)時(shí)系統(tǒng)中常見的中斷、超時(shí)和延時(shí)等概念；接著，通過(guò)一個(gè)視頻點(diǎn)播系統(tǒng)的例子來(lái)說(shuō)明利用TMSVL對(duì)實(shí)時(shí)系統(tǒng)進(jìn)行建模和性質(zhì)驗(yàn)證的具體方法；最后簡(jiǎn)單介紹了為輔助建模和驗(yàn)證而開發(fā)的一個(gè)TMSVL解釋器