软件学报
軟件學報
연건학보
JOURNAL OF SOFTWARE
2014年
2期
219-233
,共15页
混成系统%形式化方法%模型检验%定理证明
混成繫統%形式化方法%模型檢驗%定理證明
혼성계통%형식화방법%모형검험%정리증명
hybrid system%formal method%model checking%theorem proving
混成系统是实时嵌入式系统的一种重要子类,其行为中广泛存在离散控制逻辑跳转与连续实时行为交织混杂的情况,因此行为复杂,难以掌握与控制.由于此类系统广泛出现在工控、国防、交通等与国计民生密切相关的安全攸关的领域,因此,如何对相关系统进行有效的分析与理解,从而保障系统安全运营,是一项具有重要意义的工作.常规的系统安全性分析手段,如测试、仿真等仅能在一定输入的情况下运行系统来观测系统行为,无法穷尽地检测复杂混成系统在所有可能输入下的行为,因此并不足以保证系统的安全性.区别于测试等方法,形式化方法通过求解系统模型状态取值范围等方法来确认系统模型中一定不会出现相关错误.因此,其对于保障安全攸关混成系统的安全性具有十分重要的意义.形式化方法由形式化规约与形式化验证两个方面构成.因此从以上两个角度分别对形式化规约方向上现有混成系统建模语言、关注性质以及形式化验证方向的混成系统模型检验、定理证明的现有主要技术与方法进行了综述性的回顾与总结.在此基础上,针对现阶段实时嵌入式系统复杂化、网络化的特性,对混成系统形式化验证的重要关注问题与研究方向进行了探索与讨论.
混成繫統是實時嵌入式繫統的一種重要子類,其行為中廣汎存在離散控製邏輯跳轉與連續實時行為交織混雜的情況,因此行為複雜,難以掌握與控製.由于此類繫統廣汎齣現在工控、國防、交通等與國計民生密切相關的安全攸關的領域,因此,如何對相關繫統進行有效的分析與理解,從而保障繫統安全運營,是一項具有重要意義的工作.常規的繫統安全性分析手段,如測試、倣真等僅能在一定輸入的情況下運行繫統來觀測繫統行為,無法窮儘地檢測複雜混成繫統在所有可能輸入下的行為,因此併不足以保證繫統的安全性.區彆于測試等方法,形式化方法通過求解繫統模型狀態取值範圍等方法來確認繫統模型中一定不會齣現相關錯誤.因此,其對于保障安全攸關混成繫統的安全性具有十分重要的意義.形式化方法由形式化規約與形式化驗證兩箇方麵構成.因此從以上兩箇角度分彆對形式化規約方嚮上現有混成繫統建模語言、關註性質以及形式化驗證方嚮的混成繫統模型檢驗、定理證明的現有主要技術與方法進行瞭綜述性的迴顧與總結.在此基礎上,針對現階段實時嵌入式繫統複雜化、網絡化的特性,對混成繫統形式化驗證的重要關註問題與研究方嚮進行瞭探索與討論.
혼성계통시실시감입식계통적일충중요자류,기행위중엄범존재리산공제라집도전여련속실시행위교직혼잡적정황,인차행위복잡,난이장악여공제.유우차류계통엄범출현재공공、국방、교통등여국계민생밀절상관적안전유관적영역,인차,여하대상관계통진행유효적분석여리해,종이보장계통안전운영,시일항구유중요의의적공작.상규적계통안전성분석수단,여측시、방진등부능재일정수입적정황하운행계통래관측계통행위,무법궁진지검측복잡혼성계통재소유가능수입하적행위,인차병불족이보증계통적안전성.구별우측시등방법,형식화방법통과구해계통모형상태취치범위등방법래학인계통모형중일정불회출현상관착오.인차,기대우보장안전유관혼성계통적안전성구유십분중요적의의.형식화방법유형식화규약여형식화험증량개방면구성.인차종이상량개각도분별대형식화규약방향상현유혼성계통건모어언、관주성질이급형식화험증방향적혼성계통모형검험、정리증명적현유주요기술여방법진행료종술성적회고여총결.재차기출상,침대현계단실시감입식계통복잡화、망락화적특성,대혼성계통형식화험증적중요관주문제여연구방향진행료탐색여토론.
