產(chǎn)品分類 更多>>
產(chǎn)品推薦
模擬仿真能夠測試系統(tǒng)模型實(shí)現(xiàn)了我們所期望的功能，但并不能系統(tǒng)滿足安全性要求。以電梯設(shè)計(jì)為例，“電梯在運(yùn)行過程中門必須是關(guān)著的”就是安全性要求之一。由于測試的局限性，我們不可能通過模擬仿真來完全這樣的安全性，對于復(fù)雜的邏輯控制系統(tǒng)來說尤是如此。形式驗(yàn)證這一功能彌補(bǔ)了這一局限性。
詳盡的形式驗(yàn)證，不需要借助測試用例，就可以檢驗(yàn)SCADE模型達(dá)到安全性。只需在SCADE中描述安全性要求，并設(shè)置一個“特性觀察器”，用戶按一個鍵就可驗(yàn)證SCADE模型的安全性。如果模型是安全的，它能給出一個安全的證明；如果模型是不安全的，它能給出一個反例幫助我們進(jìn)行錯誤定位。形式驗(yàn)證很大程度上了目標(biāo)系統(tǒng)的安全性。
SCADE同時還內(nèi)置了兩個形式驗(yàn)證的應(yīng)用功能：除零檢查和溢出檢查，可以幫助用戶快速定位可能的除零隱患和溢出危險(xiǎn)。
公司網(wǎng)址：http://www.passiontechinc.com
