Abstract: This paper develops a robust deadlock control technique for shared and unreliable resources in automated manufacturing systems (AMSs) based on structural analysis and colored Petri nets, which consists of three steps. The first step involves using strict minimal siphon control to create a live (deadlock-free) system that does not consider resource failure. The second step uses an approach based on colored Petri net, in which all monitors designed in the first step are merged into a single monitor. The third step addresses the deadlock control problems caused by resource failures. For all resource failures in the Petri net model a common recovery subnet based on colored petri net is proposed. The common recovery subnet is added to the obtained system at the second step to make the system reliable. The proposed approach is evaluated using an AMS from the literature. The results show that the proposed approach can be applied to an unreliable complex Petri net model, has a simpler structure and less computational complexity, and can obtain one common recovery subnet to model all resource failures.
Abstract: Security of the smart home in terms of behavior activity pattern recognition is a totally dissimilar and unique issue as compared to the security issues of other scenarios. Sensor devices (low capacity and high capacity) interact and negotiate each other by detecting the daily behavior activity of individuals to execute common tasks. Once a device (e.g., surveillance camera, smart phone and light detection sensor etc.) is compromised, an adversary can then get access to a specific device and can damage daily behavior activity by altering the data and commands. In this scenario, a group of common instruction processes may get involved to generate deadlock. Therefore, an effective suitable security solution is required for smart home architecture. This paper proposes seamless distributed Scheme which fortifies low computational wireless devices for secure communication. Proposed scheme is based on lightweight key-session process to upheld cryptic-link for trajectory by recognizing of individual’s behavior activities pattern. Every device and service provider unit (low capacity sensors (LCS) and high capacity sensors (HCS)) uses an authentication token and originates a secure trajectory connection in network. Analysis of experiments is revealed that proposed scheme strengthens the devices against device seizure attack by recognizing daily behavior activities, minimum utilization memory space of LCS and avoids network from deadlock. Additionally, the results of a comparison with other schemes indicate that scheme manages efficiency in term of computation and communication.
Abstract: Workflow scheduling is an important part of cloud
computing and based on different criteria it decides cost, execution
time, and performances. A cloud workflow system is a platform
service facilitating automation of distributed applications based on
new cloud infrastructure. An aspect which differentiates cloud
workflow system from others is market-oriented business model, an
innovation which challenges conventional workflow scheduling
strategies. Time and Cost optimization algorithm for scheduling
Hybrid Clouds (TCHC) algorithm decides which resource should be
chartered from public providers is combined with a new De-De
algorithm considering that every instance of single and multiple
workflows work without deadlocks. To offset this, two new concepts
- De-De Dodging Algorithm and Priority Based Decisive Algorithm -
combine with conventional deadlock avoidance issues by proposing
one algorithm that maximizes active (not just allocated) resource use
and reduces Makespan.
Abstract: This paper presents a synthesis and simulation of proposed enhanced buffer. The design provides advantages of both buffer and bufferless network for that two cross bar switches are used. The concept of virtual channel (VC) is eliminated from the previous design by using an efficient flow-control scheme that uses the storage already present in pipelined channels in place of explicit input VCBs. This can be addressed by providing enhanced buffers on the bufferless link and creating two virtual networks. With this approach, VCBs act as distributed FIFO buffers. Without VCBs or VCs, deadlock prevention is achieved by duplicating physical channels. An enhanced buffer provides a function of hand shaking by providing a ready valid handshake signal and two bit storage. Through this design the power is reduced to 15.65% and delay is reduced to 97.88% with respect to virtual channel router.
Abstract: One major difficulty that faces developers of
concurrent and distributed software is analysis for concurrency based
faults like deadlocks. Petri nets are used extensively in the
verification of correctness of concurrent programs. ECATNets [2] are
a category of algebraic Petri nets based on a sound combination of
algebraic abstract types and high-level Petri nets. ECATNets have
'sound' and 'complete' semantics because of their integration in
rewriting logic [12] and its programming language Maude [13].
Rewriting logic is considered as one of very powerful logics in terms
of description, verification and programming of concurrent systems.
We proposed in [4] a method for translating Ada-95 tasking
programs to ECATNets formalism (Ada-ECATNet). In this paper,
we show that ECATNets formalism provides a more compact
translation for Ada programs compared to the other approaches based
on simple Petri nets or Colored Petri nets (CPNs). Such translation
doesn-t reduce only the size of program, but reduces also the number
of program states. We show also, how this compact Ada-ECATNet
may be reduced again by applying reduction rules on it. This double
reduction of Ada-ECATNet permits a considerable minimization of
the memory space and run time of corresponding Maude program.
Abstract: detecting the deadlock is one of the important
problems in distributed systems and different solutions have been
proposed for it. Among the many deadlock detection algorithms,
Edge-chasing has been the most widely used. In Edge-chasing
algorithm, a special message called probe is made and sent along
dependency edges. When the initiator of a probe receives the probe
back the existence of a deadlock is revealed. But these algorithms are
not problem-free. One of the problems associated with them is that
they cannot detect some deadlocks and they even identify false
deadlocks. A key point not mentioned in the literature is that when
the process is waiting to obtain the required resources and its
execution has been blocked, how it can actually respond to probe
messages in the system. Also the question of 'which process should
be victimized in order to achieve a better performance when multiple
cycles exist within one single process in the system' has received
little attention. In this paper, one of the basic concepts of the
operating system - daemon - will be used to solve the problems
mentioned. The proposed Algorithm becomes engaged in sending
probe messages to the mandatory daemons and collects enough
information to effectively identify and resolve multi-cycle deadlocks
in distributed systems.
Abstract: One major difficulty that faces developers of
concurrent and distributed software is analysis for concurrency based
faults like deadlocks. Petri nets are used extensively in the
verification of correctness of concurrent programs. ECATNets are a
category of algebraic Petri nets based on a sound combination of
algebraic abstract types and high-level Petri nets. ECATNets have
'sound' and 'complete' semantics because of their integration in
rewriting logic and its programming language Maude. Rewriting
logic is considered as one of very powerful logics in terms of
description, verification and programming of concurrent systems We
proposed previously a method for translating Ada-95 tasking
programs to ECATNets formalism (Ada-ECATNet) and we showed
that ECATNets formalism provides a more compact translation for
Ada programs compared to the other approaches based on simple
Petri nets or Colored Petri nets. We showed also previously how the
ECATNet formalism offers to Ada many validation and verification
tools like simulation, Model Checking, accessibility analysis and
static analysis. In this paper, we describe the implementation of our
translation of the Ada programs into ECATNets.
Abstract: There are many virtual payment systems available to
conduct micropayments. It is essential that the protocols satisfy the
highest standards of correctness. This paper examines the Netpay
Protocol [3], provide its formalization as automata model, and prove
two important correctness properties, namely absence of deadlock
and validity of an ecoin during the execution of the protocol. This
paper assumes a cooperative customer and will prove that the
protocol is executing according to its description.
Abstract: Due to important issues, such as deadlock, starvation,
communication, non-deterministic behavior and synchronization,
concurrent systems are very complex, sensitive, and error-prone.
Thus ensuring reliability and accuracy of these systems is very
essential. Therefore, there has been a big interest in the formal
specification of concurrent programs in recent years. Nevertheless,
some features of concurrent systems, such as dynamic process
creation, scheduling and starvation have not been specified formally
yet. Also, some other features have been specified partially and/or
have been described using a combination of several different
formalisms and methods whose integration needs too much effort. In
other words, a comprehensive and integrated specification that could
cover all aspects of concurrent systems has not been provided yet.
Thus, this paper makes two major contributions: firstly, it provides a
comprehensive formal framework to specify all well-known features
of concurrent systems. Secondly, it provides an integrated
specification of these features by using just a single formal notation,
i.e., the Z language.
Abstract: A new approach for timestamp ordering problem in
serializable schedules is presented. Since the number of users using
databases is increasing rapidly, the accuracy and needing high
throughput are main topics in database area. Strict 2PL does not
allow all possible serializable schedules and so does not result high
throughput. The main advantages of the approach are the ability to
enforce the execution of transaction to be recoverable and the high
achievable performance of concurrent execution in central databases.
Comparing to Strict 2PL, the general structure of the algorithm is
simple, free deadlock, and allows executing all possible serializable
schedules which results high throughput. Various examples which
include different orders of database operations are discussed.
Abstract: The approaches to make an agent generate intelligent actions in the AI field might be roughly categorized into two ways–the classical planning and situated action system. It is well known that each system have its own strength and weakness. However, each system also has its own application field. In particular, most of situated action systems do not directly deal with the logical problem. This paper first briefly mentions the novel action generator to situatedly extract a set of actions, which is likely to help to achieve the goal at the current situation in the relaxed logical space. After performing the action set, the agent should recognize the situation for deciding the next likely action set. However, since the extracted action is an approximation of the action which helps to achieve the goal, the agent could be caught into the deadlock of the problem. This paper proposes the newly developed hybrid architecture to solve the problem, which combines the novel situated action generator with the conventional planner. The empirical result in some planning domains shows that the quality of the resultant path to the goal is mostly acceptable as well as deriving the fast response time, and suggests the correlation between the structure of problems and the organization of each system which generates the action.
Abstract: Wireless mobile communications have experienced
the phenomenal growth through last decades. The advances in
wireless mobile technologies have brought about a demand for high
quality multimedia applications and services. For such applications
and services to work, signaling protocol is required for establishing,
maintaining and tearing down multimedia sessions. The Session
Initiation Protocol (SIP) is an application layer signaling protocols,
based on request/response transaction model. This paper considers
SIP INVITE transaction over an unreliable medium, since it has been
recently modified in Request for Comments (RFC) 6026. In order to
help in assuring that the functional correctness of this modification is
achieved, the SIP INVITE transaction is modeled and analyzed using
Colored Petri Nets (CPNs). Based on the model analysis, it is
concluded that the SIP INVITE transaction is free of livelocks and
dead codes, and in the same time it has both desirable and
undesirable deadlocks. Therefore, SIP INVITE transaction should be
subjected for additional updates in order to eliminate undesirable
deadlocks. In order to reduce the cost of implementation and
maintenance of SIP, additional remodeling of the SIP INVITE
transaction is recommended.
Abstract: This paper presents a new sensor-based online method for generating collision-free near-optimal paths for mobile robots pursuing a moving target amidst dynamic and static obstacles. At each iteration, first the set of all collision-free directions are calculated using velocity vectors of the robot relative to each obstacle and target, forming the Directive Circle (DC), which is a novel concept. Then, a direction close to the shortest path to the target is selected from feasible directions in DC. The DC prevents the robot from being trapped in deadlocks or local minima. It is assumed that the target's velocity is known, while the speeds of dynamic obstacles, as well as the locations of static obstacles, are to be calculated online. Extensive simulations and experimental results demonstrated the efficiency of the proposed method and its success in coping with complex environments and obstacles.