International audience

ABSTRACT Background Topology and Orchestration Specification for Cloud Applications (TOSCA) is a specification language used for modelling topology and orchestration of cloud applications. This language particularly allows the description of workflows that can be used for specifying management tasks such as (un)deployment plans. Motivations This textual language for describing TOSCA workflows does not provide any visual notation for graphically designing or observing the corresponding workflows. Moreover, this specification language is error‐prone and can be source of mistakes during the writing of the management plans. Methods In this article, we propose a transformation from TOSCA to the graphical Business Process Model and Notation (BPMN), which allows the visualisation of TOSCA workflows. We also provide automated verification techniques for analysing TOSCA (un)deployment workflows in terms of functional and architectural properties as well as execution times. The transformation and verification steps are achieved in a fully automated way. Results This approach computes BPMN models and verification results within a reasonable time on realistic applications.

IEC 61499 is a standard for developing industrial automation systems. It is known for its reusability, reconfigurability, interoperability, and portability. However, during their life cycle, industrial systems need to evolve according to requirements, and modifying the applications to satisfy these requirements can be complex and error-prone. This paper proposes techniques to guide the evolution of IEC 61499 applications. Given an initial application and the evolution requirements, we generate guidelines for modifying the application to satisfy the requirements. The application is first translated into a behavioural model describing all possible sequences of events the application can trigger. We then apply algorithms to extract relevant submodels of the application and modify them according to the requirements. Finally, the submodels are analysed to generate guidelines for modifying the application. These guidelines can bridge the gap between the requirements and the target application. Instead of only considering the requirements when exploring possible modifications, the developers can use the guidelines to make necessary changes to the application. A mixing tank system is used as a running example to illustrate the approach. In addition, a prototype to automate the evolution techniques is developed.

Abstract A business process is a collection of structured tasks corresponding to a service or a product. Business processes do not execute once and for all, but are executed multiple times resulting in multiple instances. In this context, it is particularly difficult to ensure correctness and efficiency of the multiple executions of a process. In this paper, we propose to rely on Probabilistic Model Checking (PMC) to automatically verify that multiple executions of a process respect some specific probabilistic property. This approach applies at runtime, thus the evaluation of the property is periodically verified and the corresponding results updated. However, we go beyond runtime PMC for BPMN, since we propose runtime enforcement techniques to keep executing the process while avoiding the violation of the property. To do so, our approach combines monitoring techniques, computation of probabilistic models, PMC, and runtime enforcement techniques. The approach has been implemented as a toolchain and has been validated on several realistic BPMN processes.

Resource allocation is a critical problem in business processes due to the simultaneous execution of tasks and resource sharing among them. The number of allocated resources affects both the execution cost and time of the process. In the context of runtime processes, a well-defined resource allocation strategy is essential for optimising waiting times and costs by mitigating delays and enhancing resource utilisation. This paper introduces a novel approach to dynamically adjust resource allocation during the execution of BPMN (Business Process Model and Notation) processes. The BPMN process is monitored in real-time, and the execution traces produced during its multiple executions are analysed. These execution traces are used to compute various properties or metrics of interest, including resource usage and average execution time. The approach then relies on predictive analytics to compute the future values of the aforementioned metrics. Based on these predicted results, strategies for the dynamic allocation of resources are defined, which anticipate changes in resource usage and thus dynamically update the number of resources in advance. This approach is fully automated using a toolchain and has been validated with multiple examples.

Business Process Modeling Notation (BPMN) is nowadays widely used by companies to represent their business processes. Such processes are usually designed and written by non-expert users for whom the main matter is to conceive a process corresponding to the needs of the companies. As the quality of the process is not the main design criterion, it can generally be optimised in several ways. For instance, reducing the financial cost of the process, its resource usage, or its execution time are classical optimisation axes. In this work, the considered BPMN processes are enriched with time and resources, and are executed multiple times. The proposed optimisation approach consists in reducing the execution time of these processes. To do so, the method presented in this paper consists in restructuring the processes by changing the position of their tasks. The goal of this restructuring is to limit the overuse of the resources and consequently reduce the execution time of the processes. To avoid generating unsuitable processes, the designer is involved in the restructuring phase, as (s)he validates each restructuring step. The proposed technique is fully automated by a tool that was implemented and applied on several examples for validation purposes.

This work envisions industrial control systems that can reliably adapt to requirements. We rely on the international standard IEC 61499 to achieve this goal. The standard allows downtimeless system evolution such that an application can be modified at runtime to satisfy the requirements. However, an IEC 61499 application consisting of multiple Function Blocks (FBs) can be modified in many different ways, such as inserting or deleting FBs, creating new FBs with their respective internal behaviours and adjusting the connections between FBs. These changes require considerable effort and cost, and there is no guarantee to satisfy the requirements. This article applies runtime enforcement techniques for supporting adaptive IEC 61499 applications. This set of techniques can modify the runtime behaviour of a system according to specific requirements. Our approach begins with specifying the requirements as a state machine-based notation called contract automaton. This automaton is then used to synthesise an enforcer as an FB. Finally, the new FB is integrated into the application to execute according to the requirements. A tool support is developed to automate the approach. Experiments were performed to evaluate the performance of enforcers by measuring the execution time of several applications before and after the integration of enforcers.

Business Process Model and Notation (BPMN) is a graphical modelling language for specifying business processes. Among the open issues existing in the business process development, one of them aims at providing techniques for comparing two versions of a process model. Comparing processes is useful for tackling several problems such as process reconfiguration or evolution, process harmonization or effective search. In this paper, we propose two measures of similarity between two versions of a BPMN process. The first one relies on the syntactic descriptions of the two processes considered as input, whereas the second one focuses on their semantic models. These two measures are complementary and allows users to better understand the differences and similarities between the two processes. Our approach is fully automated by several tools we reused or implemented for this work.

Consumer Internet of Things (IoT) applications are largely built through end-user programming in the form of event-action rules. Although end-user tools help simplify the building of IoT applications to a large extent, there are still challenges in developing expressive applications in a simple yet correct fashion. In this context, we propose a formal development framework based on the Web of Things specification. An application is defined using a composition language that allows users to compose the basic event-action rules to express complex scenarios. It is transformed into a formal specification that serves as the input for formal analysis, where the application is checked for functional and quantitative properties at design time using model checking techniques. Once the application is validated, it can be deployed and the rules are executed following the composition language semantics. We have implemented these proposals in a tool built on top of the Mozilla WebThings platform. The steps from design to deployment were validated on real-world applications.

The Internet of Things (IoT) is a network of physical devices and software entities that interact together for fulfilling an overall objective. Such applications are built by selecting and composing several objects. Recent frameworks promote the use of {\prime}if event(s) then action(s){\prime} rules to make explicit the way these objects interact together, i.e., if an event is raised, then an action is triggered. IoT applications are not monolithic applications built once and for all. In this paper, we focus on the replacement of an object, operation which is often required for substituting an out-of-order or obsolete device. When substituting an object by another one, the user may want the application to provide at least the same functionalities as before. Therefore, replacement should be supported by automated techniques and tools in order to guarantee the preservation of the application behaviour. As a result, we first define several notions of object substitution. Then, we show how these notions can be automatically checked or computed. Finally, we present the tool support and its integration to the Mozilla WebThings platform for applying our approach on smart home applications.

Model checking is an established technique for automatically verifying that a model satisfies a given temporal property. When the model violates the property, the model checker returns a counterexample, which is a sequence of actions leading to a state where the property is not satisfied. Understanding this counterexample for debugging the specification is a complicated task for several reasons: (i) the counterexample can contain a large number of actions, (ii) the debugging task is mostly achieved manually, and (iii) the counterexample does not explicitly highlight the source of the bug that is hidden in the model. This article presents a new approach that improves the usability of model checking by simplifying the comprehension of counterexamples. To do so, we first extract in the model all the counterexamples. Second, we define an analysis algorithm that identifies actions that make the model skip from incorrect to correct behaviours, making these actions relevant from a debugging perspective. Third, we develop a set of abstraction techniques to extract these actions from counterexamples. Our approach is fully automated by a tool we implemented and was applied on real-world case studies from various application areas for evaluation purposes.

Designing and developing distributed software has always been a tedious and error-prone task, and the ever increasing software complexity is making matters even worse. Model checking is an established technique for automatically finding bugs by verifying that a model satisfies a given temporal property. When the model violates the property, the model checker returns a counterexample, which is a sequence of actions leading to a state where the property is not satisfied. Understanding this counterexample for debugging the specification or program is a complicated task because the counterexample gives only a partial view of the source of the problem, and because there is usually little support beyond that counterexample to identify the source of the problem. In this paper, we focus on behavioural models (Labelled Transition Systems) and we propose some techniques for simplifying the debugging of erroneous models. We first focus on the erroneous part of the model and we detect specific states (called faulty states) where a choice is possible between executing a correct behaviour or falling into an erroneous part of the model. The goal of this paper is to group these faulty states into clusters. Clusters help the user to identify the source of the bug since each cluster of states provides some information about the bug. We implemented this technique into a tool, which allows the visualization of the faulty model and the computation of clusters.

This paper presents a tool for debugging behavioural models being analysed using model checking techniques. It consists of three parts: (i) one for annotating a behavioural model given a temporal formula, (ii) one for visualizing the erroneous part of the model with a specific focus on decision points that make the model to be correct or incorrect, and (iii) one for abstracting counterexamples thus providing an explanation of the source of the bug.

Fog computing provides computing, storage and communication resources at the edge of the network, near the physical world. Subsequently, end devices nearing the physical world can have interesting properties such as short delays, responsiveness, optimized communications and privacy. However, these end devices have low stability and are prone to failures. There is consequently a need for failure management protocols for IoT applications in the Fog. The design of such solutions is complex due to the specificities of the environment, i.e., (i) dynamic infrastructure where entities join and leave without synchronization, (ii) high heterogeneity in terms of functions, communication models, network, processing and storage capabilities, and, (iii) cyber-physical interactions which introduce non-deterministic and physical world's space and time dependent events. This paper presents a fault tolerance approach taking into account these three characteristics of the Fog-IoT environment. Fault tolerance is achieved by saving the state of the application in an uncoordinated way. When a failure is detected, notifications are propagated to limit the impact of failures and dynamically reconfigure the application. Data stored during the state saving process are used for recovery, taking into account consistency with respect to the physical world. The approach was validated through practical experiments on a smart home platform.

Cloud applications consist of a set of interconnected software elements distributed over several virtual machines, themselves hosted on remote physical servers. Most existing solutions for deploying such applications require human intervention to configure parts of the system, do not conform to functional dependencies among elements that must be respected when starting them, and do not handle virtual machine failures that can occur when deploying an application. This paper presents a self-deployment protocol that was designed to automatically configure a set of software elements to be deployed on different virtual machines. This protocol works in a decentralized way, that is, there is no need for a centralized server. It also starts the software elements in a certain order, respecting important architectural invariants. This protocol supports virtual machine and network failures and always succeeds in deploying an application when faced with a finite number of failures. Designing such highly parallel management protocols is difficult; therefore, formal modeling techniques and verification tools were used for validation purposes. The protocol was implemented in Java and was used to deploy industrial applications. Copyright © 2016 John Wiley & Sons, Ltd.

Choreographies are contracts specifying from a global point of view the legal interactions that must take place among a set of services. Such a contract may serve as a reference in the development of concurrent distributed system, whether it is achieved following a top-down or a bottom-up approach. In this article, we present VerChor, a generic, modular, and extensible framework for supporting the development based on choreographies. It relies on a choreography intermediate format (CIF) into which several existing choreography description languages can be transformed. VerChor builds around a set of formal properties whose verification is central to choreography-based development. To support this development process, we propose a connection between CIF and the CADP verification toolbox, which enables the full automation of the aforementioned properties. Finally, we illustrate a practical use of the VerChor framework through its integration with the Eclipse BPMN 2.0 designer.

Service-oriented computing has emerged as a new software development paradigm that enables implementation of Web accessible software systems that are composed of distributed services which interact with each other via exchanging messages. Modeling and analysis of interactions among services is a crucial problem in this domain. Interactions among a set of services that participate in a service composition can be described from a global point of view as a choreography. Choreographies can be specified using specification languages such as Web Services Choreography Description Language (WS-CDL) and visualized using graphical formalisms such as collaboration diagrams. In this paper, we present an encoding of collaboration diagrams into the LOTOS process algebra for choreography analysis. This encoding allows us to (1) check the temporal properties of choreographies using a LOTOS verification tool set called the Construction and Analysis of Distributed Processes (CADP) toolbox, (2) check the realizability of choreographies for both synchronous communication and bounded asynchronous communication, and (3) automate the peer generation process. Realizability indicates whether peers can be generated from a given choreography specification in such a way that the interactions of the generated peers exactly match the choreography specification. If a collaboration diagram is unrealizable, our approach extends the peer generation process by adding extra communication that guarantees that the peers behave according to the choreography specification.

Reuse and composition are increasingly advocated and put into practice in modern software engineering. However, the software entities that are to be reused to build an application, e.g., services, have seldom been developed to integrate and to cope with the application requirements. As a consequence, they present mismatch, which directly hampers their reusability and the possibility of composing them. Software Adaptation has become a hot topic as a nonintrusive solution to work mismatch out using corrective pieces named adaptors. However, adaptation is a complex issue, especially when behavioral interfaces, or conversations, are taken into account. In this paper, we present state-of-the-art techniques to generate adaptors given the description of reused entities' conversations and an abstract specification of the way mismatch can be solved. We use a process algebra to encode the adaptation problem, and propose on-the-fly exploration and reduction techniques to compute adaptor protocols. Our approach follows the model-driven engineering paradigm, applied to service-oriented computing as a representative field of composition-based software engineering. We take service description languages as inputs of the adaptation process and we implement adaptors as centralized service compositions, i.e., orchestrations. Our approach is completely tool supported.

Abstract Many process calculi have been proposed since Robin Milner and Tony Hoare opened the way more than 25 years ago. Although they are based on the same kernel of operators, most of them are incompatible in practice. We aim at reducing the gap between process calculi, and especially making possible the joint use of underlying tool support. Finite state processes (FSP) is a widely used calculus equipped with L tsa , a graphical and user-friendly tool. Language of temporal ordering specification (L otos ) is the only process calculus that has led to an international standard, and is supported by the C adp verification toolbox. We propose a translation of FSP sequential processes into L otos . Since FSP composite processes (i.e., parallel compositions of processes) are hard to encode directly in L otos , they are translated into networks of automata which are another input language accepted by C adp . Hence, it is possible to use jointly L tsa and C adp to validate FSP specifications. Our approach is completely automated by a translator tool.

Adaptation is of utmost importance in systems developed by assembling reusable software services accessed through their public interfaces. This process aims at solving, as automatically as possible, mismatch cases which may be given at the different interoperability levels among interfaces by synthesizing a mediating adaptor. In this paper, we present a toolbox that fully supports the adaptation process, including: (i) different methods to construct adaptation contracts involving several services; (ii) simulation and verification techniques which help to identify and correct erroneous behaviours or deadlocking executions; and (iii) techniques for the generation of centralized or distributed adaptor protocols based on the aforementioned contracts. Our toolbox relates our models with implementation platforms, starting with the automatic extraction of behavioural models from existing interface descriptions, until the final adaptor implementation is generated for the target platform.

Choreography description languages specify interactions among a set of services from a global point of view. From this description, it is possible to generate either an orchestrator (centralized interactions), or a set of peers or wrappers (distributed interactions). In this paper, we present first a model of service protocols with value passing, and an abstract choreography language to describe their composition and adaptation. Adaptation is useful while composing services to correct existing mismatches which might exist between their interfaces. Given abstract descriptions of services and their choreography, we propose techniques based on encodings into process algebra to generate an orchestrator and a set of wrapper protocols. Generation of wrappers is particularly tackled in this paper because this enables the system deployment in the context of distributed systems, and keeps at the same time a full parallelism of the system execution. Our approach is completely automated by a prototype tool we implemented.

Component-Based Software Engineering focuses on the reuse of existing software components. In practice, most components cannot be integrated directly into an application-to-be, because they are incompatible. Software Adaptation aims at generating, as automatically as possible, adaptors to compensate mismatch between component interfaces, and is therefore a promising solution for the development of a real market of components promoting software reuse. In this article, we present our approach for software adaptation which relies on an abstract notation based on synchronous vectors and transition systems for governing adaptation rules. Our proposal is supported by dedicated algorithms that generate automatically adaptor protocols. These algorithms have been implemented in a tool, called Adaptor, that can be used through a user-friendly graphical interface.

Software adaptation has been proposed as a solution to mismatch between components through the generation of software pieces called adaptors. We propose a new behavioral adaptation approach for the generation of adaptor protocols. Compared to related work, it is fully automated and addresses the adaptor computation complexity thanks to process algebra encodings and on-the-fly techniques.

Reuse of software entities such as components or web services raise composition issues since, most of the time, they present mismatching behavioural interfaces. Here, we particularly focus on systems for which the number of transactions is unbounded, and unknown in advance. This is typical in pervasive systems where a new client may show up at any moment to request or access a specific service. Hence, we advocate for the use of the pi-calculus to specify component interfaces. The pi-calculus is particularly suitable for creating new component instances and channels dynamically. The unbounded number of transactions and the use of the pi-calculus obliges to apply the composition at run-time. In this paper, we propose a run-time composition engine that solves existing mismatches.

Separation of concerns or aspects is a way to deal with the increasing complexity of systems. The separate design of models for different aspects also promotes a better reusability level. However, an important issue is then to define means to integrate them into a global model. We present a formal and tool-equipped approach for the integration of dynamic models (behaviors expressed using state diagrams) and static models (formal data types) with the benefit to share advantages of both: graphical user-friendly models for behaviors, formal and abstract models for data types. Integration is achieved in a generic way so that it can deal with both different static specification languages (algebraic specifications, Z, B) and different dynamic specification semantics

It is now widely accepted that formal methods are helpful for many issues raised in the Web services area. In this paper, we advocate the use of process algebra as a first step in the design and development of executable Web services. From such formal descriptions, reasoning tools can be used to validate their correct execution. We define some guidelines to encode abstract specifications of services-to-be written using these calculi into executable Web services. As a back-end language, we consider the standard orchestration language BPEL. We illustrate our approach through the development of an e-business application.

We argue that essential facets of Web services, and especially those useful to understand their interaction, can be described using process-algebraic notations. Web service description and execution languages such as BPEL are essentially process description languages; they are based on primitives for behaviour description and message exchange which can also be found in more abstract process algebras. One legitimate question is therefore whether the formal approach and the sophisticated tools introduced for process algebra can be used to improve the effectiveness and the reliability of Web service development. Our investigations suggest a positive answer, and we claim that process algebras provide a very complete and satisfactory assistance to the whole process of Web service development. We show on a case study that readily available tools based on process algebra are effective at verifying that Web services conform to their requirements and respect properties. We advocate their use both at the design stage and for reverse engineering issues. More prospectively, we discuss how they can be helpful to tackle choreography issues.

We introduce in (Salaun et al., 2001) the formal foundations to make a generic combination of one process algebra and one algebraic specification language possible. Furthermore, to strengthen the contribution of this work, a concrete illustration about an orders invoicing case study is detailed in (Salaun et al., 2001). In this paper, we especially focus on the addition of other languages; indeed in the initial work, we only consider a restricted number of process algebras: CCS, CSP, ACP, basic LOTOS. Therefore, we aim at formalizing the way to extend the previous combination. To achieve this goal, we present a method to enhance the syntax and semantics of the formal kernel introduced in (Salaun et al., 2001). These guidelines are illustrated with the /spl pi/-calculus.

In this paper, we suggest a formal framework as a basis for a genetic combination of formal languages. This makes it possible for the developer to specify the dynamic part of a system with a process algebra, and the static part with an algebraic specification language. The framework is based on a formal kernel composed of an abstract grammar describing the general form of the combination, and a global operational semantics giving the meaning of each language which can be built with our framework.