计算机科学
計算機科學
계산궤과학
COMPUTER SCIENCE
2011年
9期
112-115,125
,共5页
钮俊%曾国荪%吕新荣%徐畅
鈕俊%曾國蓀%呂新榮%徐暢
뉴준%증국손%려신영%서창
功能性能%连续时间Markov决策过程%模型检测%可信验证%可达概率
功能性能%連續時間Markov決策過程%模型檢測%可信驗證%可達概率
공능성능%련속시간Markov결책과정%모형검측%가신험증%가체개솔
功能正确和性能可满足是复杂系统可信要求非常重要的两个方面.从定性验证和定量分析相结合的角度,对复杂并发系统进行功能验证和性能分析,统一地评估系统是否可信.连续时间Markov决策过程CTMDP(Continuous-time Markov decision process)能够统一刻画复杂系统的概率选择、随机时间及不确定性等重要特征.提出用CTMDP作为系统定性验证和定量分析模型,将复杂系统的功能验证和性能分析转化为CTMDP中的可达概率求解,并证明验证过程的正确性,最终借助模型检测器MRMC(Markov Reward Model Checker)实现模型检测.理论分析表明,提出的针对CTMDP模型的验证需求是必要的,验证思路和方法具有可行性.
功能正確和性能可滿足是複雜繫統可信要求非常重要的兩箇方麵.從定性驗證和定量分析相結閤的角度,對複雜併髮繫統進行功能驗證和性能分析,統一地評估繫統是否可信.連續時間Markov決策過程CTMDP(Continuous-time Markov decision process)能夠統一刻畫複雜繫統的概率選擇、隨機時間及不確定性等重要特徵.提齣用CTMDP作為繫統定性驗證和定量分析模型,將複雜繫統的功能驗證和性能分析轉化為CTMDP中的可達概率求解,併證明驗證過程的正確性,最終藉助模型檢測器MRMC(Markov Reward Model Checker)實現模型檢測.理論分析錶明,提齣的針對CTMDP模型的驗證需求是必要的,驗證思路和方法具有可行性.
공능정학화성능가만족시복잡계통가신요구비상중요적량개방면.종정성험증화정량분석상결합적각도,대복잡병발계통진행공능험증화성능분석,통일지평고계통시부가신.련속시간Markov결책과정CTMDP(Continuous-time Markov decision process)능구통일각화복잡계통적개솔선택、수궤시간급불학정성등중요특정.제출용CTMDP작위계통정성험증화정량분석모형,장복잡계통적공능험증화성능분석전화위CTMDP중적가체개솔구해,병증명험증과정적정학성,최종차조모형검측기MRMC(Markov Reward Model Checker)실현모형검측.이론분석표명,제출적침대CTMDP모형적험증수구시필요적,험증사로화방법구유가행성.
