Fog computing is a new paradigm where cloud services are extended to the edge of the network. Fog nodes offer several services called fog services. These latter can accomplish Internet of Thing (IoT) applications. An IoT application is composed of a set of tasks, where each one of them can be provided by one or more fog services. In this work, we focus on the problem of assigning for each IoT task a fog service. We aim to guarantee the reliability of the assignment process. For purpose, we propose a requirements-aware fog services composition approach. Such an approach dynamically assigns tasks issued from IoT devices to a set of fog services. This assignment process is based on a set of transactions rules, which express which faults are tolerable, retriable, or recoverable. The proposed approach is based on a genetic algorithm (GA). Empirical studies are conducted to evaluate the performance of the proposed approach.

Reusability is a central concept of Web services as it allows for the construction of composite services. Thus, an existing composite service can be combined with other composite services to form more complex nested or hierarchical services. Reliability and efficiency are the main requirements of composite services construction. The reliability requirements are rigorously defined by designers using the accepted termination states concept. The efficiency requirements are tightly related to a set of quality-of-service (QoS) constraints that are required by customers. In this paper, we first developed a hierarchical model for composite services. Based on this model, we developed a recursive procedure for the automatic computation of the transactional reliability and QoS of composite services. Second, we proposed a new concept, called required efficiency level, to offer more flexibility to the customers to specify their needs in terms of QoS. Third, we developed a new composite service configuration (CSC) algorithm for the construction and adaptation of composite services while considering the reliability and efficiency requirements. The originality of the CSC algorithm consists in a new recursive global QoS constraint decomposition procedure. Finally, we conducted a set of experiments to evaluate the benefits of the proposed CSC algorithm in comparison with the related work. These experiments confirm that our CSC algorithm is able to generate, in a timely fashion, reliable, and efficient composite services.

The main issues for the fulfillment service level agreements (SLA) are concerned with problem of variability of QoS properties (vQoS). Indeed, the QoS properties may evolve frequently either because of internal changes or because of workload fluctuations. To solve the vQoS problem, we first introduced three variability operators: replicate, delete and replace. These operators will be used to reconfigure CWS when the SLA contract is violated. The first two operators are used to add and remove Web service instances, while the last one is used to substitute some faulty Web services. Then, we proposed an incremental approach for modeling and verifying the composites services (CWSs) reconfiguration using Event-B. We start by abstractly specifying the main requirements and then we refine them through several steps to model CWSs. The consistency of each model and the relationship between an abstract model and its refinements are obtained by formal proofs. Finally, we used ProB model-checker to trace possible design errors. We have exploited the LTL for dynamic reconfigurations to characterize the correct behavior of CWSs reconfiguration.

With the emergence of Service Component Architecture (SCA), all interests were focused on representing this architecture in a formal way in order to be able to prevent the specifications failures. In this context, our recent works were interested in formalizing structural properties of the SCA specifications, particularly in defining structural compatibility between connected services. In fact, verifying structural compatibility is necessary but not sufficient. In this paper we intend to represent, in a first step, the SCA behavioral properties by means of Event-B invariants and events. In a second step, we established behavioral compatibility between services interacting together which is considered as a delicate task and has a great importance in guaranteeing reliable communication between services. The consistency and the validity of the obtained model have been proved by the Event-B dedicated tools.

In this paper, we propose a new paradigm, called dynamic transactional pattern, for specifying flexible and reliable composite Web services in a pervasive environment. This new paradigm is a convergence concept of dynamic Workflow patterns and advanced transactional model. It can be seen both as a dynamic coordination and a structural transaction. Indeed, it combines dynamic Control-Flow flexibility and transactional processing reliability.

Composite applications leveraging the functionalities offered by Web services are today the underpinnings of enterprise computing. However, current Web services composition systems make only use of functional requirements in the selection process of component Web services, while the transactional consistency and quality of service (QoS) are crucial parameters of most business applications. In this paper, we propose a novel approach for Web services selection and composition based on transactional requirements and QoS constraints. The transactional requirements are defined by the engineers using the acceptable termination states concept. We give a formalization of our approach in Event-B. We incrementally combine the modeling and verification activities related to formal development process supported by Event-B method. The verification activity is based on the proof and model-checking.

Verifying Web service composition in a dynamic environment remains one of the most difficult tasks despite the efforts and the previous proposed research works because new services can be composed during the execution step and others can automatically appear, disappear, or be updated. To achieve the Web service composition specification and verification, we introduce a new concept, called dynamic pattern. A dynamic pattern is an extension of a static one. Then, we propose to formalize dynamic Web Service composition in Event-B using dynamic patterns. The resulting model is progressively verified using proofs. We use animator of model (ProB) to detect a variety of problems, such as deadlocks or other unexpected behavior of a model.