Behavioral modeling and automated verification of a Cloud-based framework to share the knowledge and skills of human resources

• Introducing the Expert Cloud to find, share, exploit, manage and employ the HR.
• Describing the state diagram of the Expert Cloud.
• Defining a Kripke structure of the Expert Cloud to provide the relationship between the expanded model and the original state diagram structure.
• Defining the expected properties of the structure and composition of the Expert Cloud by means of temporal logic languages.
• Implementing the structure and composition of the Expert Cloud by NuSMV model checker.

Expert Cloud as a new class of Cloud computing systems by employing the Internet infrastructures and Cloud computing concepts enables its users to request the skill, knowledge and expertise of human resources without any information about their location. It makes the communication between the HRs more efficient, reduces the cost of service, increases the variety of knowledge and information, facilitates employment of the HR in organizations, decreases customer response time and improves the service delivery methods. However, one facet that is still being less cared and that may introduce potential errors and faults regards the architectural problems and components analysis of Expert Cloud. Therefore, in this paper, we verify and check the specification, composition and architecture of the Expert Cloud via NuSMV model checker, Argo UML and Rebeca Verifier tools. The approach extracts the checking properties in the form of LTL and CTL formulas of control behaviors and automatically verifies the properties in operational behaviors. Also, experimental results indicate that the system is reachable, fair and deadlock-free.