上海星葩信息科技有限公司

SCADE Design Verifier（形式驗證）

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

上海星葩信息科技有限公司

錢經(jīng)理