软件学报
軟件學報
연건학보
JOURNAL OF SOFTWARE
2010年
2期
318-333
,共16页
赵常智%董威%隋平%齐治昌
趙常智%董威%隋平%齊治昌
조상지%동위%수평%제치창
运行时验证%软件监控%预测监控器%参数化LTL(linear temporal logic)%参数化Büchi自动机
運行時驗證%軟件鑑控%預測鑑控器%參數化LTL(linear temporal logic)%參數化Büchi自動機
운행시험증%연건감공%예측감공기%삼수화LTL(linear temporal logic)%삼수화Büchi자동궤
runtime verification%software monitoring%anticipatory monitor%parameterized LTL (linear temporal logic)%parameterized Büchi automata
介绍了一种基于自动机理论的参数化LTL(parameterized LTL(linear temporal logic),简称PALTL)公式运行时预测监控器构造方法.一方面研究PALTL公式的语法、预测语义、赋值提取以及赋值绑定等重要概念,从语法层面保证公式中参数化变量的正确绑定(binding)和使用(using);另一方面给出参数化预测监控器的概念.它由静态和动态两部分组成,静态部分由参数化Büchi自动机表示,动态部分为当前状态处的变量赋值.在系统运行过程中,预测监控器基于静态部分的参数化Büchi自动机,以on-the-fly的方式在当前状态处动态地提取和绑定变量赋值,递进地验证当前程序运行是否满足指定的参数化性质规约.在该过程中,参数化监控器能够精确地识别被验证性质的最小好/坏前缀.
介紹瞭一種基于自動機理論的參數化LTL(parameterized LTL(linear temporal logic),簡稱PALTL)公式運行時預測鑑控器構造方法.一方麵研究PALTL公式的語法、預測語義、賦值提取以及賦值綁定等重要概唸,從語法層麵保證公式中參數化變量的正確綁定(binding)和使用(using);另一方麵給齣參數化預測鑑控器的概唸.它由靜態和動態兩部分組成,靜態部分由參數化Büchi自動機錶示,動態部分為噹前狀態處的變量賦值.在繫統運行過程中,預測鑑控器基于靜態部分的參數化Büchi自動機,以on-the-fly的方式在噹前狀態處動態地提取和綁定變量賦值,遞進地驗證噹前程序運行是否滿足指定的參數化性質規約.在該過程中,參數化鑑控器能夠精確地識彆被驗證性質的最小好/壞前綴.
개소료일충기우자동궤이론적삼수화LTL(parameterized LTL(linear temporal logic),간칭PALTL)공식운행시예측감공기구조방법.일방면연구PALTL공식적어법、예측어의、부치제취이급부치방정등중요개념,종어법층면보증공식중삼수화변량적정학방정(binding)화사용(using);령일방면급출삼수화예측감공기적개념.타유정태화동태량부분조성,정태부분유삼수화Büchi자동궤표시,동태부분위당전상태처적변량부치.재계통운행과정중,예측감공기기우정태부분적삼수화Büchi자동궤,이on-the-fly적방식재당전상태처동태지제취화방정변량부치,체진지험증당전정서운행시부만족지정적삼수화성질규약.재해과정중,삼수화감공기능구정학지식별피험증성질적최소호/배전철.
