基于組合IIS路徑抽取的組合線性混成系統(tǒng)有界可達(dá)性分析-中國(guó)科學(xué)

中國(guó)科學(xué): 信息科學(xué) 2017 年 第47 卷 第3 期: 288–309

論文

基于組合 路徑抽取的組合線性混成系統(tǒng)有界

可達(dá)性分析優(yōu)化

1 1 1,2 1,2 1,2

解定寶 周岳翔 卜磊 王林章 李宣東

1. 南京大學(xué)計(jì)算機(jī)軟件新技術(shù)國(guó)家重點(diǎn)實(shí)驗(yàn)室, 南京 210023

2. 江蘇省軟件新技術(shù)與產(chǎn)業(yè)化協(xié)同創(chuàng)新中心, 南京 210023

* 通信作者. E-mail: bulei@

收稿日期: 2016–03–02; 接受日期: 2016–05–31; 網(wǎng)絡(luò)出版日期: 2016–09–14

國(guó)家重點(diǎn)基礎(chǔ)研究發(fā)展計(jì)劃(973) (批準(zhǔn)號(hào): 2014CB340703) 和國(guó)家自然科學(xué)基金 (批準(zhǔn)號(hào): 61561146394,

資助項(xiàng)目

摘要 混成系統(tǒng)是一類(lèi)同時(shí)具有離散和連續(xù)行為的復(fù)雜系統(tǒng) 被廣泛應(yīng)用于控制系統(tǒng)建模 針對(duì)其

安全性需求 對(duì)不安全狀態(tài)進(jìn)行有界可達(dá)性驗(yàn)證 是保障系統(tǒng)安全的重要手段 然而 當(dāng)前技術(shù)所能

處理的問(wèn)題規(guī)模和現(xiàn)實(shí)生活里的實(shí)際需要尚有一定的距離 特別是組合混成系統(tǒng)由于涉及到各個(gè)組

件間的協(xié)作與同步 組合狀態(tài)空間快速爆炸 對(duì)其進(jìn)行驗(yàn)證具有極高的復(fù)雜性 為控制問(wèn)題的復(fù)雜

度 一種面向路徑的可達(dá)性分析方法在前期工作中被提出用來(lái)對(duì)組合線性混成系統(tǒng)進(jìn)行有界可達(dá)性

分析 該方法通過(guò)依次枚舉潛在路徑并進(jìn)行驗(yàn)證的方式 有效地提升了所能處理的問(wèn)題規(guī)模 當(dāng)面對(duì)

復(fù)雜系統(tǒng)時(shí) 上述面向路徑的檢測(cè)方法將會(huì)因?yàn)榇龣z測(cè)路徑數(shù)量的急劇上升而使得驗(yàn)證效率大幅降

低 這也是模型檢驗(yàn)狀態(tài)空間爆炸問(wèn)題的一種體現(xiàn) 為解決此問(wèn)題 本文提出了一種狀態(tài)空間約減

技術(shù)以加速驗(yàn)證過(guò)程 當(dāng)一組路徑被判定為不可行時(shí) 定位出導(dǎo)致其不可行的原因 得到一個(gè)組合

不可行路徑片段 由于包含同樣片段的組合路徑一定不可行 因此在后續(xù)的路徑遍歷里只需要枚舉

與檢驗(yàn)不包含組合不可行路徑片段的路徑 從而大幅減少需要檢驗(yàn)的路徑數(shù)量 此外 為了有效地

規(guī)避此類(lèi)組合路徑片段 我們?cè)O(shè)計(jì)了一種全新的基于 編碼的有界圖結(jié)構(gòu)遍歷方法 實(shí)驗(yàn)表明

該優(yōu)化技術(shù)大幅地提升了面向路徑有界可達(dá)性分析方法的性能 整體性能也超越了當(dāng)前最先進(jìn)的同

類(lèi)工具

關(guān)鍵詞 混成系統(tǒng) 有界模型檢驗(yàn) 可達(dá)性分析 組合線性混成自動(dòng)機(jī) 可滿足性 不可約不可解

子集

引言

混成系統(tǒng) 是一類(lèi)同時(shí)具有離散和連續(xù)行為特征的復(fù)雜系統(tǒng) 被廣泛應(yīng)用于工業(yè)

控制系統(tǒng)的建模 近年來(lái) 隨著軟件失效帶來(lái)的損失越來(lái)越大 人們對(duì)于系統(tǒng)的安全性要求越來(lái)越高

引用格式 解定寶 周岳翔 卜磊 等 基于組合 路徑抽取的組合線性混成系統(tǒng)有界可達(dá)性分析優(yōu)化 中國(guó)科學(xué) 信息科學(xué)

? 《中國(guó)科學(xué)》雜志社

中國(guó)科學(xué): 信息科學(xué) 第47 卷 第 3 期

尤其是安全攸關(guān)領(lǐng)域 幾乎已經(jīng)到了零容忍的地步 模型檢驗(yàn) 是一種可以自動(dòng)化

發(fā)現(xiàn)系統(tǒng)錯(cuò)誤的高效方法 其基本思想是遍歷系統(tǒng)模型的狀態(tài)空間 找出所有可能的錯(cuò)誤 是保障系

統(tǒng)質(zhì)量的重要手段 當(dāng)前 混成自動(dòng)機(jī) 是一種廣泛使用的混成系統(tǒng)建模語(yǔ)言 因

此 對(duì)混成自動(dòng)機(jī)進(jìn)行模型檢驗(yàn)是相關(guān)領(lǐng)域的一個(gè)重要問(wèn)題 由于混成自動(dòng)機(jī)里離散與連續(xù)行為的混

雜交織 相應(yīng)的模型檢驗(yàn)問(wèn)題十分困難 比如 即使是混成自動(dòng)機(jī)的一個(gè)相對(duì)簡(jiǎn)單的子類(lèi) 線性混

總結(jié)

以上是生活随笔為你收集整理的岳翔南京大学计算机,基于组合IIS路径抽取的组合线性混成系统有界可达性分析-中国科学.PDF...的全部?jī)?nèi)容，希望文章能夠幫你解決所遇到的問(wèn)題。

如果覺(jué)得生活随笔網(wǎng)站內(nèi)容還不錯(cuò)，歡迎將生活随笔推薦給好友。