主页期刊介绍编委会编辑部服务介绍道德声明在线审稿编委办公编辑办公English
2018-2019年专刊出版计划 微信服务介绍 最新一期:2018年第12期
     
在线出版
各期目录
纸质出版
分辑系列
论文检索
论文排行
综述文章
专刊文章
美文分享
各期封面
E-mail Alerts
RSS
旧版入口
中国科学院软件研究所
  
投稿指南 问题解答 下载区 收费标准 在线投稿
胡 军,黄志球,曹 东,徐丙凤.网构软件的资源自适应性的形式化分析与验证.软件学报,2008,19(5):1186-1200
网构软件的资源自适应性的形式化分析与验证
Formal Analysis and Verification of Resource Adaptability for Internetware
投稿时间:2007-11-15  修订日期:2008-03-19
DOI:
中文关键词:  网构软件  构件式设计  资源自适应  形式化验证  统一建模语言
英文关键词:Internetware  component-based design  resource adaptive  formal verification  UML
基金项目: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 (高等学校博士学科点专项科研基金)
作者单位
胡 军 南京航空航天大学 信息科学与技术学院,江苏 南京 210016
南京大学 计算机软件新技术国家重点实验室,江苏 南京 210093 
黄志球 南京航空航天大学 信息科学与技术学院,江苏 南京 210016 
曹 东 南京航空航天大学 自动化学院,江苏 南京 210016 
徐丙凤 南京航空航天大学 信息科学与技术学院,江苏 南京 210016 
摘要点击次数: 6023
全文下载次数: 4009
中文摘要:
      针对基于构件的网构软件系统对环境资源变化的自适应性特征的可信分析与验证展开研究.具体工作包括:在网构软件的系统模型层次,使用带资源语义信息的接口自动机对软件构件的行为进行形式化建模,其包含了构件在完成特定功能的过程中对环境资源的使用特征;使用资源接口自动机网络来描述构件组装实体的组合行为;使用基于场景的UML顺序图模型来描述具有多功能的组合系统规约;分别研究了检验组合系统的所有行为是否都满足给定的资源约束以及检验指定的系统行为是否满足资源约束这两个具体问题;通过对资源自动机网络状态空间的分析,构造其相应的可达图,在此基础上给出了相应的检验资源可满足性、最小资源需求量以及检验指定功能合法性等算法.
英文摘要:
      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.
HTML  下载PDF全文  查看/发表评论  下载PDF阅读器
 

京公网安备 11040202500064号

主办单位:中国科学院软件研究所 中国计算机学会
编辑部电话:+86-10-62562563 E-mail: jos@iscas.ac.cn
Copyright 中国科学院软件研究所《软件学报》版权所有 All Rights Reserved
本刊全文数据库版权所有,未经许可,不得转载,本刊保留追究法律责任的权利