In this special issue of Concurrency and Computation: Practice and Experience (CCPE), we focus on three complementary aspects that have to be considered while setting up future Internet services: (i) their modeling, provisioning, and management; (ii) data protection; and (iii) data collection, storage, and analysis.The special issue includes extended versions, containing at least 50% new material of selected accepted papers from the Future Internet Services and Applications(FISA) track of the 29th IEEE WETICE Conference.It also includes four new submissions dealing with FISA-related issues.In total, we received 11 submissions from six different countries.After two rounds of reviews, we accepted seven articles: four enhancing the quality of the papers.

Artificial Intelligence (AI) and data are reshaping organizations and businesses. Human Resources (HR) management and talent development make no exception, as they tend to involve more automation and growing quantities of data. Because this brings implications on workforce, career transparency, and equal opportunities, overseeing what fuels AI and analytical models, their quality standards, integrity, and correctness becomes an imperative for those aspiring to such systems. Based on an ontology transformation to B-machines, this article presents an approach to constructing a valid and error-free career agent with Deep Reinforcement Learning (DRL). In short, the agent's policy is built on a framework we called Multi State-Actor (MuStAc) using a decentralized training approach. Its purpose is to predict both relevant and valid career steps to employees, based on their profiles and company pathways (observations). Observations can comprise various data elements such as the current occupation, past experiences, performance, skills, qualifications, and so on. The policy takes in all these observations and outputs the next recommended career step, in an environment set as the combination of an HR ontology and an Event-B model, which generates action spaces with respect to formal properties. The Event-B model and formal properties are derived using OWL to B transformation.

The “Future Internet Services and Applications” (FISA) track focuses on three complementary aspects that have to be considered while setting up future Internet services: (i) their modeling, provisioning and management, (ii) data protection, and (iii) data collection, storage and analysis. FISA is in its fifth edition and aims at offering to academic and industrial researchers as well as practitioners a platform for discussions related to the aforementioned aspects of future Internet services and applications. This report briefly presents the main topics of FISA and lists the accepted papers.

Summary The software‐as‐a‐service layer of cloud computing has evolved much interest among the researchers in the academic and industry worlds. It is based on service‐oriented architectures and web service (WS) technology, which are used to offer a remotely accessible application. When a single WS is unable to satisfy all the customer's requirements, a WS composition (WSC) method is applied to connect together various available WSs for building distributed application, using discovery, compatibility checking, selection, and deployment steps. This paper has two‐fold contributions: The major one is the proposition of a new algorithm based on minimally unsatisfiable subset formal algorithm to compose WSs. This contribution ensures a faster WSC, which is prominent in an online context. The second contribution is the proposition of a new penalty‐based genetic algorithm to identify near‐optimal solutions whenever an exact one is not identified using our formal algorithm. Indeed, in some cases, many available WSs provide overlapping/identical functionality; in this context, the choice of participated services is given using quality of service. This work proposes a WSC ensuring to find out an exact or a near‐optimal solution according to the user need. A set of experimentations is applied to validate our contributions.

Nowadays, tremendous number of enterprises are looking to outsource their business processes in order to gain in productivity, reduce cost, and enhance performance. Outsourcing business processes to cloud computing and more specifically to SaaS services, is actually among the most prominent opportunities regarding the benefits that this paradigm offers. However, matching the business process activities with the suitable SaaS services is not a trivial task regarding the diversity of both, functional requirements of business processes and the functionalities offered by SaaS services. Furthermore, once the business process execution is entirely supported by the SaaS services, the process owner, lacking in general the required expertise related to SaaS domain, needs to be aware of how the business process is handled by the SaaS. This is done principally through transforming the business process model to the SaaS model. This paper proposes a model-based approach using SAT-based formal verification to select and validate the most suitable SaaS services to support the business process achievement. Furthermore, a model to model transformation from business process to SaaS is proposed. This transformation is based on (i) a lightweight extension of the business process meta-model of ISO/CEI 19510 and (ii) our proposition of the SaaS meta-model.

Formalizing system specification has been highly valuable in demonstrating safety and consistence of safety critical systems. It is undoubtedly the case in railway signalling, especially the European Rail Traffic Management System/European Train Control System (ERTMS/ETCS). However, the complexity of the European standard specification, especially for its highest level, namely level 3, requires a significant overtake in early modelling approaches when it comes to clearly expressing system functionalities along with safety requirements, all towards a concrete safe design. In this regard, our research introduces a Colored Petri net (CPN) sub-class associated to an Event-B machine and annotated by mathematical sequences, which are ex-pressed in the B-language, all in the view of enriching the modelling techniques intended for system formal specification and verification. In this paper, we show through a detailed ERTMS L3 case study, how such featured CPNs fit in the progressive formalization and verification of Movement Authority (MA) computation.

International audience

Business Process as a Service (BPaaS) is knowing a considerable proliferation and an exponential emergence as a new Cloud service for delivering complex and complete business applications. In order to guarantee a place in the actual harshly competitive Cloud services, BPaaS providers should offer to their clients, flexible services responding both to their functional and non-functional requirements. In this paper, we propose a Reconfigurable BPaaS based SaaS services Federation system (RBPF). The reconfiguration allows for a flexible BPaaS service responding to the changing users functional and non-functional requirements. To do so, the RBPF system follows the Boolean Satisfiability Problem (SAT) based algorithms to (i) initially configure the Business process based on SaaS services and to (ii) reconfigure minimally and on the fly the composition whenever a reconfiguration is required. The end users of the RBPF system are BPaaS as well as SaaS providers (a federation of SaaS) aiming to collaborate for the BPaaS achievement purpose.

A Software Product Line (SPL) is a tool/method used to generate a family of program/system variants for a specific domain, and to support a more efficient software development of future products within the same domain. A Feature Model (FM) is a popular graphical/textual representation used in SPL requirements specification; it is used to capture commonality and variability information existing in an SPL as a set of inter-related and configurable features. A concrete model of an SPL instance is obtained by binding the variation information in the FM with a configuration that meets a specific set of feature requirements. Since configuration decisions are taken prior to instantiation, invalid configurations should be detected/avoided before design begins. This paper addresses the problem of the verification of the correctness (validity) of FM instances and FM configuration during requirements modelling. It proposes a requirements model based on Event-B contexts, allowing us to check the correctness of a given configuration, before starting the correct-by-construction design and implementation process, based on refinement.

Component-based approach is a programming paradigm well-suited to design complex applications. In particular, this paradigm offers and promotes interesting capabilities in terms of the separation of concerns. For that, it allow the building of applications made of very heterogeneous codes. With component-based approach, developing an application consists in assembling many different components which is a difficult task. Thus, it is important to design efficient tools to help the user to conceive his application and to verify some properties as deadlock-freedom or liveness. In this paper, we present Component-based approach for Scientific Applications (ComSA) and its formalization in a particular class of FIFO nets called strict colored FIFO nets (sCFN). We present also our ComSATool plateform based on sCFN and in particular the analysis part to detect deadlocks and to construct a start condition of the ComSA applications.

Cloud Computing based Software as a Service (SaaS) combines multiple Web Services to satisfy a SaaS request. SaaS is based on Service-Oriented Architecture and Web Service technology which are popular paradigm to design new generation of applications. One of the advantages of Web Services technology is to building distributed application on demand using existing service oriented application. Web Services Composition (WSC) in Cloud Computing is necessary when a single service is unable to satisfy all the customers requirements. WSC is a complex task in the SaaS which involves several steps like discovery, compatibility checking, selection and deployment. To reduce the complexity of WSC, we model Web Services and their composition using Boolean satisfiability problem so that a specific property of their structures is looked into behavioral compatibility. The aim of this work is the modelling and verification of Web Services Composition using a formal method based on Satisfiability (SAT). However, in some cases it may be preferable to use variations of the general SAT problem. Specifically, using the Minimally Unsatisfiable Subformula (MUS), we formally define a Web Services Composition and its validation. When we have a multiple Web Services Compositions that meet the users needs, a QoS of the resulting WSC is maximized or, in some cases, minimized.

Cloud Computing-based Software as a Service (SaaS) combines multiple Web Services in order to satisfy an SaaS request. SaaS is based on service-oriented architecture and Web Service technology which are popular paradigm to design new generation of applications. In addition, SaaS composition can maintain Data as a Service (DaaS) to answer the needs of a customer that cannot be satisfied by a single Web Service. SaaS/DaaS composition may reveal privacy sensitive information. In this paper, we propose a formal model of privacy in order to verify compatibility of services involved in this composition in terms of their privacy capabilities. We propose a new technique that translates the problem of minimum SaaS/DaaS Web Services Composition within preserved-privacy into Satisfiability problem. We propose also a generalization of this approach to take into account the Quality of Service. In order to show that our approach is feasible and efficient in practice, experiment results are provided as a benchmark.

Cloud Computing based Software as a Service (SaaS) combines multiple Web Services to satisfy a SaaS request, therefore SaaS should be able to dynamically seek replacements for faulty or underperforming services, thus performing self-healing. However, it may be the case of available services that do not match all user's request, leading the system to grind to a halt. It is better to have an alternative candidate in the cloud while not fulfilling all the constraints. In this paper, we provide a solution to repair the failed user's query by rewriting it with an approximation. It is based on a Minimally Unsatisfiable Subformula (MUS) that exploits Satisfiability (SAT) problem to repair the query and provide an alternative SaaS that leads to a successful request closed to the original one.

Cloud Computing based Software as a Service (SaaS) combines multiple Web Services in order to satisfy a SaaS request. SaaS is based on Service Oriented Architectures and Web Service technology which are popular paradigm to design new generation of applications. These functionalities are published on the Internet, but exploiting rigorously a large data stream in order to use Web Services is a complicated and laborious task which may involve error prone. In this paper we investigate the problem of SaaS Web Service Composition. We present a new technique that combines an encoding into SAT and a Minimal Unsatisfiability Subformulas extraction to obtain the minimum SaaS Web Service Composition. Furthermore, we generalize this approach to take into account the quality of SaaS Web Service.