In the last decade, cloud computing has emerged as one of the most popular computing models. This model delivers a pool of computing resources as on-demand services to different categories of users. As the number of cloud services available on the Internet is increasing and owing to the users' complicated requirement, the composition of cloud services has become more and more challenging. In this work, we are interested in the vertical composition that represents the collaboration of services from different cloud layers to offer a complete solution to end-users. This paper proposes the Bigraphical Reactive Systems (BRS) to model the service composition. We use bigraphs to describe the different actors and services evolving in the composition. In addition, we define a set of bigraphical reactive rules to express the dynamic behaviors of these services and actors and to show the direct and indirect dependencies between them.

In order to automate Business Processes Modeling, the last research works in workflow technology have resulted in the identification of a number of models (workflow patterns) that describe the behavior of Business Processes. Like any new trend, the Business Process approach raises many expectations and many positions. BPMN (Business Process Modeling Notation) has been used to describe graphically such patterns. However, BPMN notation lacks verification tools which allow anomalies and errors detection such as deadlock and multiple repetition situations. On the other hand, formal methods, such as Pi-Calculus, have powerful tools for verifying such situations. In this paper, we propose an automatic approach to transform the basic workflow patterns into their equivalent Pi-Calculus code for the analysis purposes. To achieve this goal, we use the Model-Driven Engineering (MDE) approach which is mainly based on Meta-modeling and Model Transformations. The graph transformation tool AToM3 is used. Our approach is illustrated through an example.

In Reconfigurable Manufacturing Systems (RMSs), the structure of the system can be changed during execution of the system. This reconfiguration can be motivated by a new requirement in the production process, or to avoid some problems caused by machines breakdowns. These systems offer a high flexibility leading to more productivity and efficiency. However, their design is more complicated implying new techniques and paradigms. The use of formal high level Petri Nets offers the ability to design these systems and to analyse or prove their properties. In this paper, we apply Reconfigurable Object Nets (RONs) for the modelling, simulation and analysis of reconfigurable manufacturing systems. We propose a formal approach, where the reconfiguration is specified as graph transformations, the simulation is realized using the RON-tool, and the analysis exploits some software tools such as TINA-tool and PIPE-tool.

Using Petri nets to model reconfigurable systems, where structure changes during runtime, have been one of the research axes in high level Petri nets domain. Numerous formalisms with different particularities have been proposed. These formalisms try to deal with some aspects of these systems. In the present paper, we propose a new PNets-based formalism “Flexible Nets” that we consider more general and more adequate to model reconfigurable systems. The current formalism allows to the net to be flexible and its structure can be changed with few constraints. Places, transitions, and arcs can be added and deleted from the net during its execution. These qualities will offer to the developer a sophisticated tool to model easily his system. We present the formal definition of the formalism, a case study on a real and complex system, and then we will discuss some analysis and verification issues.

In this paper we propose an approach for transforming UML statechart and collaboration diagrams to colored Petri nets models. This transformation aims to bridge the gap between informal notation (UML diagrams) and more formal notation (colored Petri nets models) for analysis purpose. It produces highly-structured, graphical, and rigorously-analyzable models that facilitates early detection of errors like deadlock, livelock, etc ... The approach is based on graph transformation since the input and output of the transformation process are graphs. The meta-modeling tool ATOM3is used. An example illustrates our approach.

This paper deals with the problem of causal model-based diagnosis of distributed systems. The setting we consider is a collection of interacting behavioral Petri nets (BPNs). Each BPN model represents the causal behavioral model of one subsystem and its interactions with neighboring subsystems. Interactions among subsystems are modeled by tokens that pass from one model to another via common places. Diagnosis reasoning scheme exploits, in a first step a backward reachability analysis on each net model to obtain local diagnoses; and in a second step, it exploits a forward reachability analysis for ensuring that local diagnoses are consistent and form global ones.