计算机技术与发展
計算機技術與髮展
계산궤기술여발전
COMPUTER TECHNOLOGY AND DEVELOPMENT
2010年
5期
34-38
,共5页
高洪皓%宫尚%王鹏%陈韶君
高洪皓%宮尚%王鵬%陳韶君
고홍호%궁상%왕붕%진소군
高可靠性与可信性%马丁洛夫类型理论与Coq%形式化组装验证%服务构件
高可靠性與可信性%馬丁洛伕類型理論與Coq%形式化組裝驗證%服務構件
고가고성여가신성%마정락부류형이론여Coq%형식화조장험증%복무구건
服务构件的组装和验证是基于构件的软件工程的核心.为确保服务构件组装的高可靠性,引入了马丁洛夫类型理论来形式化地描述构件接口的功能性和非功能语义信息,使之在进行组装时,可利用其接口所携带的语义并根据推理规则在验证工具Coq中推导其正确性和可信性.其次,提出基于类型理论的组装验证模型并结合实例进行分析.最后,介绍了文中的可视化开发平台的原型系统,其具有界面友好、功能操作简单等特点.通过马丁洛夫类型理论的方法组合的构件系统表现出高可靠性.
服務構件的組裝和驗證是基于構件的軟件工程的覈心.為確保服務構件組裝的高可靠性,引入瞭馬丁洛伕類型理論來形式化地描述構件接口的功能性和非功能語義信息,使之在進行組裝時,可利用其接口所攜帶的語義併根據推理規則在驗證工具Coq中推導其正確性和可信性.其次,提齣基于類型理論的組裝驗證模型併結閤實例進行分析.最後,介紹瞭文中的可視化開髮平檯的原型繫統,其具有界麵友好、功能操作簡單等特點.通過馬丁洛伕類型理論的方法組閤的構件繫統錶現齣高可靠性.
복무구건적조장화험증시기우구건적연건공정적핵심.위학보복무구건조장적고가고성,인입료마정락부류형이론래형식화지묘술구건접구적공능성화비공능어의신식,사지재진행조장시,가이용기접구소휴대적어의병근거추리규칙재험증공구Coq중추도기정학성화가신성.기차,제출기우류형이론적조장험증모형병결합실례진행분석.최후,개소료문중적가시화개발평태적원형계통,기구유계면우호、공능조작간단등특점.통과마정락부류형이론적방법조합적구건계통표현출고가고성.
