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

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. (C) 2015 Elsevier B.V. All rights reserved.