计算机研究与发展
計算機研究與髮展
계산궤연구여발전
JOURNAL OF COMPUTER RESEARCH AND DEVELOPMENT
2011年
6期
913-922
,共10页
贾仰理%李舟军%邢建英%陈石坤
賈仰理%李舟軍%邢建英%陳石坤
가앙리%리주군%형건영%진석곤
构件%模型检验%形式化描述%验证%可信性质
構件%模型檢驗%形式化描述%驗證%可信性質
구건%모형검험%형식화묘술%험증%가신성질
模型检验以其自动化程度和完备性高、与构件技术互补性强等特点,在软件构件可信性质的分析和验证中发挥着日益重要的作用.将基于模型检验的构件验证方法分为基于系统规约模型的验证和基于源代码的验证,分别对其研究现状和发展动态进行了详细的综合评述.首先对模型检验与构件可信性质验证的关系进行了探讨,接着对基于SOFA,Fractal,CORBA及各种特定构件模型的验证方法和基于转化思想的源码验证、面向源码的直接验证及面向可执行代码的动态验证方法分别进行了评述.最后,指出了基于模型检验的构件验证技术所面临的主要挑战和未来的发展方向.
模型檢驗以其自動化程度和完備性高、與構件技術互補性彊等特點,在軟件構件可信性質的分析和驗證中髮揮著日益重要的作用.將基于模型檢驗的構件驗證方法分為基于繫統規約模型的驗證和基于源代碼的驗證,分彆對其研究現狀和髮展動態進行瞭詳細的綜閤評述.首先對模型檢驗與構件可信性質驗證的關繫進行瞭探討,接著對基于SOFA,Fractal,CORBA及各種特定構件模型的驗證方法和基于轉化思想的源碼驗證、麵嚮源碼的直接驗證及麵嚮可執行代碼的動態驗證方法分彆進行瞭評述.最後,指齣瞭基于模型檢驗的構件驗證技術所麵臨的主要挑戰和未來的髮展方嚮.
모형검험이기자동화정도화완비성고、여구건기술호보성강등특점,재연건구건가신성질적분석화험증중발휘착일익중요적작용.장기우모형검험적구건험증방법분위기우계통규약모형적험증화기우원대마적험증,분별대기연구현상화발전동태진행료상세적종합평술.수선대모형검험여구건가신성질험증적관계진행료탐토,접착대기우SOFA,Fractal,CORBA급각충특정구건모형적험증방법화기우전화사상적원마험증、면향원마적직접험증급면향가집행대마적동태험증방법분별진행료평술.최후,지출료기우모형검험적구건험증기술소면림적주요도전화미래적발전방향.
