一種基于模型轉(zhuǎn)換的狀態(tài)機(jī)模型時(shí)序性質(zhì)驗(yàn)證系統(tǒng)

基本信息

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

摘要

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