软件学报
軟件學報
연건학보
JOURNAL OF SOFTWARE
2015年
4期
730-746
,共17页
软件自适应%自适应软件%软件建模%形式化验证
軟件自適應%自適應軟件%軟件建模%形式化驗證
연건자괄응%자괄응연건%연건건모%형식화험증
software self-adaptation%self-adaptive software%software modeling%formal verification
软件自适应的建模和形式化验证是提高自适应软件开发效率、保证自适应软件可靠性的基础,现有研究中软件自适应可视化建模与形式化建模相隔离,一定程度上阻碍了自适应软件的开发.为此,提出MV4SAS的方法,将可视化的UML与严格化的时间自动机相结合,用于软件自适应的建模和形式化验证.首先,应用UML扩展机制引入新的构造型、标记值和约束条件,定义软件自适应建模设施,在此基础上构造软件自适应结构模型和行为模型;然后,根据定义好的转换算法将软件自适应行为模型转换为时间自动机网络,建立软件自适应形式化模型;最后,定义一组软件自适应形式化验证性质,并利用模型检测工具UPPAAL验证软件自适应模型的可靠性.案例研究表明,该方法可有效降低软件自适应建模和验证的复杂度,提高软件自适应的建模效率和模型可靠性.
軟件自適應的建模和形式化驗證是提高自適應軟件開髮效率、保證自適應軟件可靠性的基礎,現有研究中軟件自適應可視化建模與形式化建模相隔離,一定程度上阻礙瞭自適應軟件的開髮.為此,提齣MV4SAS的方法,將可視化的UML與嚴格化的時間自動機相結閤,用于軟件自適應的建模和形式化驗證.首先,應用UML擴展機製引入新的構造型、標記值和約束條件,定義軟件自適應建模設施,在此基礎上構造軟件自適應結構模型和行為模型;然後,根據定義好的轉換算法將軟件自適應行為模型轉換為時間自動機網絡,建立軟件自適應形式化模型;最後,定義一組軟件自適應形式化驗證性質,併利用模型檢測工具UPPAAL驗證軟件自適應模型的可靠性.案例研究錶明,該方法可有效降低軟件自適應建模和驗證的複雜度,提高軟件自適應的建模效率和模型可靠性.
연건자괄응적건모화형식화험증시제고자괄응연건개발효솔、보증자괄응연건가고성적기출,현유연구중연건자괄응가시화건모여형식화건모상격리,일정정도상조애료자괄응연건적개발.위차,제출MV4SAS적방법,장가시화적UML여엄격화적시간자동궤상결합,용우연건자괄응적건모화형식화험증.수선,응용UML확전궤제인입신적구조형、표기치화약속조건,정의연건자괄응건모설시,재차기출상구조연건자괄응결구모형화행위모형;연후,근거정의호적전환산법장연건자괄응행위모형전환위시간자동궤망락,건립연건자괄응형식화모형;최후,정의일조연건자괄응형식화험증성질,병이용모형검측공구UPPAAL험증연건자괄응모형적가고성.안례연구표명,해방법가유효강저연건자괄응건모화험증적복잡도,제고연건자괄응적건모효솔화모형가고성.
