###
DOI:
Journal of Software:2008.19(5):1186-1200

网构软件的资源自适应性的形式化分析与验证
胡军,黄志球,曹东,徐丙凤
(南京航空航天大学 信息科学与技术学院,江苏 南京 210016; 南京大学 计算机软件新技术国家重点实验室,江苏 南京 210093;南京航空航天大学 自动化学院,江苏 南京 210016)
Formal Analysis and Verification of Resource Adaptability for Internetware
HU Jun,HUANG Zhi-Qiu,CAO Dong,XU Bing-Feng
()
Abstract
Chart / table
Reference
Similar Articles
Article :Browse 7350   Download 4510
Received:November 15, 2007    Revised:March 19, 2008
> 中文摘要: 针对基于构件的网构软件系统对环境资源变化的自适应性特征的可信分析与验证展开研究.具体工作包括:在网构软件的系统模型层次,使用带资源语义信息的接口自动机对软件构件的行为进行形式化建模,其包含了构件在完成特定功能的过程中对环境资源的使用特征;使用资源接口自动机网络来描述构件组装实体的组合行为;使用基于场景的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.
文章编号:     中图分类号:    文献标志码:
基金项目: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 (高等学校博士学科点专项科研基金) 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 (高等学校博士学科点专项科研基金)
Foundation items:
Reference text:

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

HU Jun,HUANG Zhi-Qiu,CAO Dong,XU Bing-Feng.Formal Analysis and Verification of Resource Adaptability for Internetware.Journal of Software,2008,19(5):1186-1200