基于模型的网构软件可达性检测方法研究

摘要

Aim at the challenge of exploded state space where an Internet Ware is searched by using the method of model checking, a new method based on the algebraic model of Internet Ware for checking his reachability is proposed.With respect to the attributes of Internet Ware an algebraic model is proposed first, and then it is fully developed by introducing a series of new concept, for example Internet Ware Correlative and Internet Ware Space.By discovering the relationship between reachability of Internet ware software and Internet ware Operation Expression,converts the reachability of Internet ware software into the recursion of Internet ware Operation Expression.By mapping the Internet Ware Space to Linear Space translates his linear correlativity checking into solving his equations.All above effort can cut the volume of spaces down dramatically with proposed algorithm.Finally, the application aspects of checking method are discussed too.%针对网构软件(Internetware)可达性检测中存在状态空间"爆炸"等问题,提出了一种基于网构软件代数模型的可达性检测方法.根据网构软件特性建立其代数模型,通过引入网构相关和网构空间概念,进一步扩展网构软件代数模型.通过明确网构软件可达性与网构组合运算表达式的关系,把可达性判定转化成递归表达式(网构线性相关)判定上来;通过建立网构空间到线性空间映射,把网构线性相关判定问题转化成齐次线性方程组非零解的判定上来.转换过程把线性相关的网构进行压缩,从而有效地抑制了状态空间的增长.给出了可达性检测算法,并讨论了该方法的实际应用.