计算机应用 ›› 2012, Vol. 32 ›› Issue (11): 3067-3070.DOI: 10.3724/SP.J.1087.2012.03067

• 计算机软件 • 上一篇    下一篇

网构软件的随机性资源自适应性的形式化分析与验证

夏琦1,王忠群2   

  1. 1. 安徽工程大学, 计算机与信息学院,安徽 芜湖 241000
    2. 安徽工程大学 计算机与信息学院,安徽 芜湖 241000
  • 收稿日期:2012-05-28 修回日期:2012-07-18 发布日期:2012-11-12 出版日期:2012-11-01
  • 通讯作者: 夏琦
  • 作者简介:夏琦(1988-),男,安徽马鞍山人,硕士研究生,主要研究方向:软件工程;王忠群(1965-),男,安徽芜湖人,教授,主要研究方向:软件工程、分布式计算、工作流技术。
  • 基金资助:
    国家自然科学基金资助项目(61071087);安徽省自然科学基金资助项目(070412058)

Formal analysis and verification of randomness resources for Internetware

XIA Qi1,WANG Zhong-qun2   

  1. 1. School of Computer and Information, Anhui Polytechnic University, Wuhu Anhui 241000,China
    2. School of Computer and Information, Anhui Polytechnic University, Wuhu Anhui 241000, China
  • Received:2012-05-28 Revised:2012-07-18 Online:2012-11-12 Published:2012-11-01
  • Contact: XIA Qi

摘要: 因特网上的资源具有不确定性、随机性,需要考虑如何保证网构软件系统在运行中满足资源需求。使用随机性资源接口自动机对软件构件的行为进行形式化建模,并使用随机性资源接口自动机网络描述构件组装系统的组合行为;在资源不确定的情况下,检验组合系统是否满足资源约束,并提出基于可达图的相应算法。给出了一个实例网上书店系统,并用模型检测工具Spin验证了模型的正确性。

关键词: 网构软件, 随机性资源, 接口自动机, 可达图

Abstract: The resources on Internet are uncertain and random, which poses a challenge on how to guarantee that requirements of the resources are met for an Internetware system at run time. The interface automata with randomness resources was used to model the behaviors of software component, and the combination behavior of component assembly system was described using the randomness resources interface automata networks. Under the circumstance of resources with uncertainty and randomness, whether all the behaviors of a system were satisfied within the specified resource constraints was checked. And a reached graph based algorithm was proposed. Finally, the online bookstore system was used to illustrate the work, and the model checker Spin was used to verify the correctness of the proposed approach.

Key words: Internetware, randomness resources, interface automata, reached graph

中图分类号: