In the curriculum of a Computer Engineering program, concepts like parallelism, concurrency, consistency, or atomicity are usually addressed in separate courses due to their thoroughness and extension. Isolating such concepts in courses helps students not only to focus on specific aspects, but also to experience the reality of working with modern computer systems, where those concepts are often detached in different abstraction levels. However, due to such an isolation, it exists a risk of inducing to the students an absence of interactions between these concepts, and, by extension, between the different abstraction levels of a system. This paper proposes a learning experience showcasing the interactions between abstraction levels addressed in laboratory sessions of different courses. The driving example is a parallel ray tracer. In the different courses, students implement and assemble components of this application from the algorithmic level of the tracer to the assembly instructions required to guarantee atomicity. Each lab focuses on a single abstraction level, but shows students the interactions with the rest of the levels. Technical results and student learning outcomes through the analysis of surveys validate the proposed experience and confirm the students learning improvement with a more integrated view of the system.

The decision of migrating a service to a cloud-based system must take into consideration many different aspects. Among them, economical costs is one of the most important. This paper describes how a computing-intensive service, based on a bag-of-tasks approach, has been migrated from a grid infrastructure to the Amazon Elastic Compute Cloud (EC2) infrastructure. A cost-based model for the evaluation of the economic costs of providing the service on the cloud has also been proposed, which considers computing costs as well as storage and platform deployment costs. The model includes a wide range of different instance types and purchasing policies provided by the Amazon EC2, as well as the deadline and problem size provided by the service user. The paper also shows how the proposed cost-based model is integrated into the framework used for the service deployment and execution, making possible the interaction with the Amazon Web services for hiring the required cloud resources and efficiently use them for the execution of the service requests.

Motivation: To attain acceptable sample misassignment rates, current approaches to multiplex single-molecule real-time sequencing require upstream quality improvement, which is obtained from multiple passes over the sequenced insert and significantly reduces the effective read length. In order to fully exploit the raw read length on multiplex applications, robust barcodes capable of dealing with the full single-pass error rates are needed. Results: We present a method for designing sequencing barcodes that can withstand a large number of insertion, deletion and substitution errors and are suitable for use in multiplex single-molecule real-time sequencing. The manuscript focuses on the design of barcodes for full-length single-pass reads, impaired by challenging error rates in the order of 11%. The proposed barcodes can multiplex hundreds or thousands of samples while achieving sample misassignment probabilities as low as 10-7 under the above conditions, and are designed to be compatible with chemical constraints imposed by the sequencing process. Availability and Implementation: Software tools for constructing watermark barcode sets and demultiplexing barcoded reads, together with example sets of barcodes and synthetic barcoded reads, are freely available at www.cifasis-conicet.gov.ar/ezpeleta/NS-watermark . Contact: [email protected].

Summary Formal verification plays a crucial role when dealing with correctness of systems. In a previous work, the authors proposed a class of models, the Unary Resource Description Framework Petri Nets (U‐RDF‐PN), which integrated Petri nets and (RDF‐based) semantic information. The work also proposed a model checking approach for the analysis of system behavioural properties that made use of the net reachability graph. Computing such a graph, specially when dealing with high‐level structures as RDF graphs, is a very expensive task that must be considered. This paper describes the development of a parallel solution for the computation of the reachability graph of U‐RDF‐PN models. Besides that, the paper presents some experimental results when the tool was deployed in cluster and cloud frameworks. The results not only show the improvement in the total time required for computing the graph, but also the high scalability of the solution, which make it very useful thanks to the current (and future) availability of cloud infrastructures. Copyright © 2016 John Wiley & Sons, Ltd.

Cyber Physical Society (CPS) feature a tight integration between computation, communication, and control in their operation and interactions with the environment in which they are deployed. The concept of capability, which is the semantics of an action or specific functionality, is therefore a cornerstone in modern Cyber Physical Society, especially those service or process aware. In this track, we present dedicated techniques for capability management and engineering, which can be applied and reused in a large number of areas such as SOA, BPM, Cloud Computing and Internet of Things. These techniques will certainly boost several related research efforts in Cyber Physical Society. This track aims at shedding the light on the importance of capability engineering as well as at bringing together researchers and practitioners working in capability engineering to achieve the vision of cyber physical society by means of current techniques.

Cyber Physical Society (CPS) feature a tight integration between computation, communication, and control in their operation and interactions with the environment in which they are deployed. The concept of capability, which is the semantics of an action or specific functionality, is therefore a cornerstone in modern Cyber Physical Society, especially those service or process aware. In this track, we present dedicated techniques for capability management and engineering, which can be applied and reused in a large number of areas such as SOA, BPM, Cloud Computing and Internet of Things. These techniques will certainly boost several related research efforts in Cyber Physical Society. This track aims at shedding the light on the importance of capability engineering as well as at bringing together researchers and practitioners working in capability engineering to achieve the vision of cyber physical society by means of current techniques.

Semantic business processes require new analysis techniques able to deal with behavioral properties that also consider semantic aspects. In this paper, a model checking method is introduced including semantic aspects in both the model description and the formula to be verified. In addition, Unary resource description framework (RDF) annotated Petri net systems, a formalism that allows the semantic description of business processes using RDF annotations, is formally defined and used to represent the input model of the model checker. Finally, the prototype implementations of both the Unary RDF annotated Petri net formalism and a model checker framework based on the use of RDF and SPARQL tools are also presented.

SUMMARY Service‐oriented computing provides a suitable technological foundation for developing and executing dynamic business processes. However, most current approaches for composition languages and architectures for dynamic process integration do not provide the flexibility and dynamism required by interorganisational evolving environments. In this work, the DENEB platform for the development and execution of Web processes is presented. DENEB is based on the conversational approach and the Nets‐within‐Nets paradigm, allowing Web processes to acquire and execute new interaction protocols at run‐time. This makes DENEB a well‐adapted and flexible platform for dynamic service composition, interaction and integration, suitable for this kind of scenario. The scalability of the proposed solution is evaluated by means of the development of a set of experiments. Copyright © 2011 John Wiley & Sons, Ltd.

Abstract In the coming years, one of the challenges for business processes is to obtain a high degree of flexibility and ability to adapt to the changing contexts. Two key elements for achieving this are the use of Semantic Web technologies and the possibility of decoupling the business and the interaction aspects in a business process. Nevertheless, these solutions open up new challenges related to the necessity of checking whether a set of processes can successfully cooperate. Compatibility questions should be considered from a control flow point of view (the order of the interactions should be appropriate) and also from a data flow point of view (the information exchanged should be—semantically—adequate). In this paper, we concentrate on the compatibility of a set of processes executed in DENEB, a platform for the Development and ExecutioN of wEB processes based on the Net‐within‐Nets formalism and that follows a conversational approach. More specifically, this paper examines whether a set of interactions among a set of processes is compatible and also whether a given (imposed) interaction logic is compatible with a given business logic. Processes and their interactions have been semantically enhanced by means of domain ontologies and compatibility questions are studied using standard Petri net analysis techniques. Copyright © 2010 John Wiley & Sons, Ltd.

Abstract One of the basic problems in (semantic) business process management concerns the behavioral analysis at design time so that only correct processes are exposed. Although this analysis requires the semantic propagation of data and system preconditions through processes and between processes to be considered, some concrete data are usually obtained at runtime and cannot be used in early process development phases. This paper proposes Parametric Unary RDF Annotated Petri Net Systems (P‐U‐RDF‐PN Systems) as a formalism to alleviate this problem. The formalism allows analyzing behavioral properties of semantic business processes at design time. Parametric values are used to represent the data that will be obtained at runtime, allowing to also consider them in the analysis phase. The paper formally defines the semantics of the formalism in terms of enabling and firing of transitions as well as the concept of reachability graph. It also presents how to compute and analyze this parametric reachability graph. The analysis is based on an adaption of model checking techniques, being temporal logic the formalism used to specify the system properties to be analyzed. Finally, an implementation prototype using RDF and SPARQL tools and a Satisfiability Modulo Theories solver is presented, with some experiments evaluating how scalable the prototype is. Copyright © 2010 John Wiley & Sons, Ltd.

Abstract Scientific workflow systems often operate in highly unreliable, heterogeneous and dynamic environments, and have accordingly incorporated different fault tolerance techniques. We propose an exception‐handling mechanism, based on techniques adopted in programming languages, for modifying at run‐time the structure of a workflow. In contrast to other proposals that achieve the required flexibility by means of the infrastructure, our proposal expresses the exception‐handling mechanism within the workflow language—primarily as two exception‐handling patterns that are exclusively based on the Reference Nets‐within‐Nets formalism (a specific type of Petri nets). When an exception is detected, a workflow in our approach can be re‐written (replaced), based on the particular failure condition that has been detected. This enables workflow users to have better control and understanding of the behaviour of their workflow without having to be aware of the underlying infrastructure. Copyright © 2009 John Wiley & Sons, Ltd.

The activities developed by a company (business processes) have to change frequently to adapt to the environment. The implementation of business processes should support these changes without any recoding. In this work, we provide with an approach for modelling and executing agile and adaptable business processes. Our approach is based on UML 2 separating choreography (stable interaction patterns) and orchestration (implementation of the evolving business process, also called workflows), allowing the transformation and execution of the models by means of a flexible SOA-based dynamic platform based on reference Petri nets.

There is growing interest in promoting interoperability among the many different existent Grid initiatives. The requirements for interlinking of Grids have already been studied from a general point of view. In this paper, we analyse current practice in Grid interactions and show evidence of how Grid interactions may represent a barrier for interlinking of Grids. Our proposal consists of three combined aspects: a) explicitly modelling the interactions (what we call interaction protocols), b) decoupling the execution flow of services from their interactions with other services and c) services have to be able to dynamically select the interaction protocol at the time they have decided to interact with another party. Next, for a clarifying purpose, we show how DVega, an application built on the proposed principles, can use these features as the foundations for interacting with disparate services from different Grids in a flexible and dynamic way.

This correspondence introduces a deadlock-avoidance algorithm for a class of manufacturing systems with the following characteristics: 1) Production orders are allowed to have assembly operations (which give the nonsequential nature to the resource allocation system model) but not disassembly operations, 2) the use of system resources must be conservative (resources are neither created nor destroyed), and 3) actions related to the granting of resources are controllable. The proposed solution represents a sufficient condition for a given system state to be safe and is based on an adaptation of the well-known Banker's approach for deadlock avoidance. The time complexity of the proposed solution is proved to be polynomial with the size of the Place/Transition net model.

Siphons are related to the liveness properties of Petri net models. This relation is strong in the case of resource allocation systems (RASs). Siphons can be used in these systems in order to both characterize and prevent/avoid deadlock situations. However, the computation of these structural components can be very time consuming or, even, impossible. Moreover, if, in general, the complete enumeration of the set of minimal siphons must be avoided (there can exist an exponential number of such components), some deadlock prevention methods rely on its (complete or partial) computation and enumeration. The special syntactical constraints of some classes of RASs can help in developing specific algorithms to compute siphons in a more efficient way. In this work, a known method for siphon computation is adapted to get advantage of the special (syntactical) structure of a class of RASs; a parallel implementation is proposed and some experimental results are presented

A new method for the deadlock prevention problem in concurrent systems where a set of processes share a set of common resources in a conservative way is proposed. It can be applied to flexible manufacturing systems, modeled with Petri nets. In this paper, we present a set of important results related to the deadlock prevention problem in S4PR nets. First, a liveness characterization is introduced, establishing how deadlocks can be studied in terms of circular waits. Second, we show how a circular wait situation corresponds to a particular marking related to a siphon of the Petri net model. Finally, this last characterization is used to obtain an iterative method that successively forbids deadlock related states, synthesizing the control necessary to ensure a final live behavior. The method can be implemented by means of the solutions of a set of integer linear programming problems.

The paper concentrates on the deadlock-avoidance problem for a class of resource allocation systems modeling manufacturing systems. In these systems, a set of production orders have to be executed in a concurrent way. To be executed, each step of each production order needs a set of reusable system resources. The competition for the use of these resources can lead to deadlock problems. Many solutions, from different perspectives, can be found in the literature for deadlock-related problems when the production orders have a sequential nature [sequential resource allocation systems (S-RAS)]. However, in the case in which the involved processes have a nonsequential nature [nonsequential resource allocation systems (NS-RAS)], the problem becomes more complex. In this paper, we propose a deadlock avoidance algorithm for this last class of systems. We also show the usefulness of the proposed solution by means of its application to a real system.

Siphons are related to liveness properties of Petri net models. This relation is strong in the case of resource allocation systems (RAS). Siphons can be used in these systems in order to both, characterize and prevent/avoid deadlock situations. However, the computation of these structural components can be very time consuming or, even, impossible. Moreover, if, in general, the complete enumeration of the set of minimal siphons must be avoided (there can exist an exponential number of such components), some deadlock prevention methods rely on its (complete or partial) computation and enumeration. In the paper we show how the special syntactical constraints of some classes of resource allocation systems (we concentrate on S/sup 4/PR) can help in developing specific implementations to compute siphons in a very efficient way.

Banker's-like approaches to deadlock avoidance are based on a decision procedure to grant active processes resources using information about the maximum needs of resources that a process can request in order to ensure termination. The paper presents an extension of the classical Banker's algorithm to a class of flexible manufacturing systems modeled by means of Petri nets. These systems have two interesting characteristics from the application point of view. First, flexible routing of parts is allowed, and second, a multiset of resources is allowed to be used at each processing step. The decision procedure introduced is polynomial in the Petri net model size.

The paper presents two methods for deadlock avoidance in concurrent systems. We apply the proposed approaches to flexible manufacturing systems, modeled by means of Petri nets. Both methods correspond to improvements of the classical Banker's algorithm, and are based on the knowledge of the process structure. The first one is polynomial in the size of the Petri net model. The second one depends strongly on the number of alternative paths for the processing of parts and can be of a non-polynomial cost.

In this paper we research a modeling methodology, applicable to a large class of flexible manufacturing systems (FMS), that takes advantage of the differentiation between the FMS layout and the set of process plans corresponding to the different types of parts to be processed, We propose a separate modeling of these two components. In a second step, both models are integrated automatically in a unique model, represented as a colored Petri net (CPN). The second aim of the paper is the application of a deadlock prevention control policy ensuring that the processing of each part can be completed.

In this paper we illustrate a compositional method for modeling the concurrent execution of working processes in flexible manufacturing systems (FMS) through a special class of Petri nets that we call S/sup 3/PR. In essence, this class is built from state machines sharing a set of places modeling the availability of system resources. The analysis of S/sup 3/PR leads us to characterize deadlock situations in terms of a zero marking for some structural objects called siphons. In order to prevent the system from deadlocks, we propose a policy for resource allocation based on the addition of new places to the net imposing restrictions that prevent the presence of unmarked siphons (direct cause of deadlocks). Finally we present the application of this technique to a realistic FMS case.>