一種基于模型轉(zhuǎn)換的狀態(tài)機(jī)模型時序性質(zhì)驗證方法

基本信息

申請?zhí)?/td> CN201910606311.5 申請日 -
公開（公告）號 CN110532167A 公開（公告）日 2019-12-03
申請公布號 CN110532167A 申請公布日 2019-12-03
分類號 G06F11/36 分類 計算；推算；計數(shù);
發(fā)明人 黃滟鴻;史建琦;張繼;郭欣;施健 申請（專利權(quán)）人 上海豐蕾信息科技有限公司
代理機(jī)構(gòu) 北京辰權(quán)知識產(chǎn)權(quán)代理有限公司 代理人 劉廣達(dá)
地址 200062 上海市普陀區(qū)中山北路3663號
法律狀態(tài) -

摘要

摘要 本申請公開了一種基于模型轉(zhuǎn)換的狀態(tài)機(jī)模型時序性質(zhì)驗證方法，包括：模型解析步驟，解析SCADE文本模型，得到語法樹實例；符號表容器步驟，裝載語法樹實例，得到符號表實例；模型轉(zhuǎn)換步驟，根據(jù)模型轉(zhuǎn)換規(guī)則將符號表實例轉(zhuǎn)換為NuSMV模型；模型檢查步驟，根據(jù)LTL公式及CTL公式驗證NuSMV模型的時序性質(zhì)。通過解析高安全性的應(yīng)用程序開發(fā)環(huán)境SCADE文本模型，將SCADE文本模型轉(zhuǎn)換為NuSMV模型，根據(jù)LTL公式及CTL公式驗證NuSMV模型的時序性質(zhì)，從而實現(xiàn)驗證SCADE文本模型的時序性質(zhì)，突破了SCADE模型性質(zhì)驗證的這個限制，進(jìn)一步提高軟件系統(tǒng)的安全性與可靠性。通過為SCADE形式化驗證引入能夠描述時序相關(guān)安全需求的時序規(guī)范，從而能夠驗證模型的時序性質(zhì)。