网构软件的资源自适应性的形式化分析与验证
DOI:
作者:
作者单位:

作者简介:

通讯作者:

中图分类号:

基金项目:

Supported by the Foundation of Aeronautics Science of China under Grant No.2007ZD52043 (航空科学基金); the Foundation of the Special Research Fund for the Doctoral Program of Higher Education of China under Grant No.20070287052 (高等学校博士学科点专项科研基金)


Formal Analysis and Verification of Resource Adaptability for Internetware
Author:
Affiliation:

Fund Project:

  • 摘要
  • |
  • 图/表
  • |
  • 访问统计
  • |
  • 参考文献
  • |
  • 相似文献
  • |
  • 引证文献
  • |
  • 资源附件
  • |
  • 文章评论
    摘要:

    针对基于构件的网构软件系统对环境资源变化的自适应性特征的可信分析与验证展开研究.具体工作包括:在网构软件的系统模型层次,使用带资源语义信息的接口自动机对软件构件的行为进行形式化建模,其包含了构件在完成特定功能的过程中对环境资源的使用特征;使用资源接口自动机网络来描述构件组装实体的组合行为;使用基于场景的UML顺序图模型来描述具有多功能的组合系统规约;分别研究了检验组合系统的所有行为是否都满足给定的资源约束以及检验指定的系统行为是否满足资源约束这两个具体问题;通过对资源自动机网络状态空间的分析,构造其相应的可达图,在此基础上给出了相应的检验资源可满足性、最小资源需求量以及检验指定功能合法性等算法.

    Abstract:

    This paper considers the formal analysis and verification methods for the environmental resource adaptability of component-based Interneware. Firstly, the resource interface automata is used to model the behaviors of component interfaces which contain the information of dynamical resource utilization, and the resource interface automaton networks are constructed to describe the compositional behaviors of the system. At the same time, the UML sequence diagrams are used to model the specifications of specified behaviors in the compositional system. Then, two typical problems are proposed and analyzed formally, one of them is to check whether all behaviors of a system are satisfied within the specified resource constraints, and the other is the verification of whether the specified behaviors are satisfied when the resources have been changed. Based on analyzing the compatible state space of the resource interface automata networks, a corresponding reachability graph is constructed, and finally several algorithms are developed for the above problems.

    参考文献
    相似文献
    引证文献
引用本文

胡 军,黄志球,曹 东,徐丙凤.网构软件的资源自适应性的形式化分析与验证.软件学报,2008,19(5):1186-1200

复制
分享
文章指标
  • 点击次数:
  • 下载次数:
  • HTML阅读次数:
  • 引用次数:
历史
  • 收稿日期:2007-11-15
  • 最后修改日期:2008-03-19
  • 录用日期:
  • 在线发布日期:
  • 出版日期:
您是第位访问者
版权所有:中国科学院软件研究所 京ICP备05046678号-3
地址:北京市海淀区中关村南四街4号,邮政编码:100190
电话:010-62562563 传真:010-62562533 Email:jos@iscas.ac.cn
技术支持:北京勤云科技发展有限公司

京公网安备 11040202500063号