A formal approach for the specification and verification of a Trustworthy Human Resource Discovery mechanism in the Expert Cloud

• Proposing a method for Trustworthy Human Resource Discovery (THRD) in Expert Cloud.
• Verifying the compositions of THRD by behavioral models and state diagrams.
• Defining a Kripke structure of the compositions of THRD.
• Defining the properties of the compositions of THRD by temporal logic languages.
• Implementing the proposed model by NuSMV model checker.

Expert Cloud as a new class of Cloud computing systems enables its users to request the skill, knowledge and expertise of people without any information of their location by employing Internet infrastructures and Cloud computing concepts. One of the most important service in Expert Cloud is to search trustworthy peoples in order to benefit from their knowledge and skills. In this paper we propose a new and applicable method for Trustworthy Human Resource Discovery (THRD) in Expert Cloud by introducing a resource discovery and trust evaluating method, implement the proposed method by using ASP.Net and SQL in Expert Cloud; verify the structures and compositions of THRD by describing the behavioral models and state diagrams; define a Kripke structure with marked states to provide the formal relationship between the expanded model and the original state diagram structures; define the expected properties of the structures and compositions of THRD by means of temporal logic languages; and implement the proposed model by NuSMV model checker. The results show that the proposed method can discover trustworthy people efficiently and is sound, complete, reachable, fair, deadlock-free and consistent.