Behavioral modeling and formal verification of a resource discovery approach in Grid computing

作者：

Highlights：

• Presenting a resource discovery approach to address multi-attribute and range queries.

• Modeling the behaviors of proposed approach.

• Analyzing the soundness, completeness, and consistency as a model checking problem.

• Translating the design model into a verifiable formal model.

• Implementing the behavior models by ArgoUML tool and the NuSMV model checker.

摘要

•Presenting a resource discovery approach to address multi-attribute and range queries.•Modeling the behaviors of proposed approach.•Analyzing the soundness, completeness, and consistency as a model checking problem.•Translating the design model into a verifiable formal model.•Implementing the behavior models by ArgoUML tool and the NuSMV model checker.

论文关键词：Grid computing,Formal verification,Behavioral modeling,Resource discovery,Model checking,NuSMV

论文评审过程：Available online 11 December 2013.

论文官网地址：https://doi.org/10.1016/j.eswa.2013.11.042