%0 Journal Article %A 王忠群 %A 夏琦 %T 网构软件的随机性资源自适应性的形式化分析与验证 %D 2012 %R 10.3724/SP.J.1087.2012.03067 %J 计算机应用 %P 3067-3070 %V 32 %N 11 %X 因特网上的资源具有不确定性、随机性,需要考虑如何保证网构软件系统在运行中满足资源需求。使用随机性资源接口自动机对软件构件的行为进行形式化建模,并使用随机性资源接口自动机网络描述构件组装系统的组合行为;在资源不确定的情况下,检验组合系统是否满足资源约束,并提出基于可达图的相应算法。给出了一个实例网上书店系统,并用模型检测工具Spin验证了模型的正确性。 %U http://www.joca.cn/CN/10.3724/SP.J.1087.2012.03067