Synchronizability of conversations among Web services

We present a framework for analyzing interactions among Web services that communicate with asynchronous messages. We model the interactions among the peers participating in a composite Web service as conversations, the global sequences of messages exchanged among the peers. This naturally leads to the following model checking problem: Given an LTL property and a composite Web service, do the conversations generated by the composite Web service satisfy the property? We show that asynchronous messaging leads to state space explosion for bounded message queues and undecidability of the model checking problem for unbounded message queues. We propose a technique called synchronizability analysis to tackle this problem. If a composite Web service is synchronizable, its conversation set remains the same when asynchronous communication is replaced with synchronous communication. We give a set of sufficient conditions that guarantee synchronizability and that can be checked statically. Based on our synchronizability results, we show that a large class of composite Web services with unbounded message queues can be verified completely using a finite state model checker such as SPIN. We also show that synchronizability analysis can be used to check the reliability of top-down conversation specifications and we contrast the conversation model with the Message Sequence Charts. We integrated synchronizability analysis to a tool we developed for analyzing composite Web services.     

Schedulability analysis for Controller Area Network (CAN) with FIFO queues priority queues and gateways

Controller Area Network (CAN) is widely used in automotive applications. Existing schedulability analysis for CAN is based on the assumption that the highest priority message ready for transmission at each node on the network will be entered into arbitration on the bus. However, in practice, some CAN device drivers implement FIFO rather than priority-based queues invalidating this assumption. In this paper, we introduce response time analysis and optimal priority assignment policies for CAN messages in networks where some nodes use FIFO queues while other nodes use priority queues. We show, via a case study and experimental evaluation, the detrimental impact that FIFO queues have on the real-time performance of CAN. Further, we show that in gateway applications, if it is not possible to implement a priority queue, then it is preferable to use multiple FIFO queues each allocated a small number of messages with similar transmission deadlines.     

Optimal routing into two heterogeneous service stations withdelayed information

The problem of optimal routing of messages into two parallel queues is considered in the framework of discrete-time Markov decision processes with countable state space and unbounded costs. We assume that the controller has a delayed state information, the delay being equal to one time slot. Both discount and average optimal policies are shown to be monotone and of threshold type     

Recent Advances in Real-Time Maude

This paper gives an overview of recent advances in Real-Time Maude. Real-Time Maude extends the Maude rewriting logic tool to support formal specification and analysis of object-based real-time systems. It emphasizes ease and generality of specification and supports a spectrum of analysis methods, including symbolic simulation, unbounded and time-bounded reachability analysis, and LTL model checking. Real-Time Maude can be used to specify and analyze many systems that, due to their unbounded features, such as unbounded data structures or dynamic object and message creation, cannot be modeled by current timed/hybrid automaton-based tools. We illustrate this expressiveness and generality by summarizing two case studies: (i) an advanced scheduling algorithm with unbounded queues; and (ii) a state-of-the-art wireless sensor network algorithm. Finally, we give some (often easily checkable) conditions that ensure that Real-Time Maude's analysis methods are complete, also for dense time, for object-based real-time systems. In practice, our result implies that Real-Time Maude's time-bounded search and model checking of LTL time-bounded formulas are complete decision procedures for a large and useful class of non-Zeno real-time systems that fall outside the scope of systems that can be modeled in decidable fragments of hybrid automata, including the sensor network case study discussed in this paper.     

基于BitTorrent协议Have消息的信息隐藏方法

针对以比特流（BitTorrent）协议消息为载体的信息隐藏算法在隐蔽性和嵌入容量上所存在的问题,提出一种以Have消息序列为载体的信息隐藏方法。首先,在秘密信息嵌入前设置容量分析模块,判断信息嵌入量是否超出信息隐藏容量上限;其次,在信息嵌入时使用改进的奇偶映射信息编码方式,将秘密信息嵌入到Have消息的排序中;最后,在信息提取时引入循环冗余校验（CRC）方法,验证秘密信息是否传输正确。实验结果表明,相比原有的奇偶映射编码方式,所提方法的嵌入容量明显提高,且通过对Have序列统计特性的分析,所提方法对Have序列统计特性的影响较小,隐蔽性较强。     

Multicasting in the presence of aggregated deliveries

An increasing number of distributed systems relies on forms of message correlation, which result in atomic delivery of multiple messages aggregated by following process-specific criteria. Generally, more than one process is aggregating messages, implying that messages are multicast. While delivery guarantees for multicast scenarios with single message delivery are well understood, existing systems and models for aggregated deliveries either consider only unicast, centralized setups, or focus on efficiency thus providing only best-effort guarantees. This paper investigates the foundations of Multi-Delivery Multicast (MDMcast) in asynchronous distributed systems with crash-stop failures. We first describe a succinct aggregation model with a concise and generic predicate grammar for expressing conjunctions on messages and properties for a corresponding multicast primitive, which we term Conjunction-MDMcast (C-MDMcast). We show that for processes interested in identical conjunctions to achieve agreement on delivered messages, a total order on individual messages (or equivalent oracle) is not only useful but necessary, which is clearly opposed to single-message deliveries. We show this indirectly by exhibiting an algorithm implementing C-MDMcast on top of Total Order Broadcast (TOBcast) and vice-versa for a majority of correct processes. Then, we extend our predicate grammar with disjunctions, leading to the specification of Disjunction-MDMcast (D-MDMcast). We exhibit an algorithm implementing D-MDMcast, derived from our algorithm implementing C-MDMcast. We formalize several additional properties for both of our specifications, including ordering properties on aggregated messages and a notion of agreement capturing non-identical yet “related” conjunctions, and show how our respective algorithms implement these.     

Optimal tracing and replay for debugging message-passing parallel programs

A common debugging strategy involves reexecuting a program (on a given input) over and over, each time gaining more information about bugs. Such techniques can fail on message-passing parallel programs. Because of nondeterminacy, different runs on the given input may produce different results. This nonrepeatability is a serious debugging problem, since an execution cannot always be reproduced to track down bugs. This paper presents a technique for tracing and replaying message-passing programs. By tracing the order in which messages are delivered, a reexecution can be forced to deliver messages in their original order, reproducing the original execution. To reduce the overhead of such a scheme, we show that the delivery'order of only messages involved inraces need be traced (and not every message). Our technique makes run-time decisions to detect and trace racing messages and is usuallyoptimal in the sense that the minimal number of racing messages is traced. Experiments indicate that only 1% of the messages are often traced, gaining a reduction of two orders of magnitude over traditional techniques that trace every message. These traces allow an execution to be reproduced any number of times for debugging. Our work is novel in that we adaptively decide what to trace, and trace only those messages that introduce nondeterminacy. With our strategy, large reductions in trace size allow long-running programs to be replayed that were previously unmanageable. In addition, the reduced tracing requirements alleviate tracing bottle-necks, allowing executions to be debugged with substantially lower execution time overhead.This work was supported in part by National Science Foundation grants CCR-8815928 and CCR-9100968, Office of Naval Research grant N00014-89-J-1222, and a grant from Sequent Computer Systems, Inc.     

Rollback recovery in distributed systems using loosely synchronizedclocks

A rollback recovery scheme for distributed systems is proposed. The state-save synchronization among processes is implemented by bounding clock drifts such that no state-save synchronization messages are required. Since the clocks are only loosely synchronized, the synchronization overhead can be negligible in many applications. An interprocess communication protocol which encodes state-save progress information within message frames is introduced to checkpoint consistent system states. A rollback recovery algorithm that will force a minimum number of nodes to roll back after failures is developed     

On the analysis of a symmetric polling system with single-message buffers

A performance analysis is provided for a polling system consisting of statistically identical stations with single-message buffers and Poisson arrival streams. Switchover and message service times are assumed to be generally distributed. Some errors in the past analysis are pointed out. We express such performance measures as the mean polling cycle time, the mean message response time, and the mean number of messages at an arbitrary time in terms of the mean number of massages served in a polling cycle. Our mean message response time reduces to that for an FCFS M/G/1//N queue (machine interference model) in the limit of zero switchover time.     

两级嵌入式系统的消息驱动和快速传送

提出了两级调度嵌入式操作系统的运行原理和任务、子任务的消息驱动机制,设计了一种新的描述消息的数据结构,用以满足两级调度嵌入式操作系统的运行.利用这种数据结构,可以用零拷贝的方式来传送消息,极大地提高了系统的效率.在两级嵌入式操作系统中,构建了完全独立的、由不同类型消息所组成的任务级消息队列和子任务级消息队列.最后,分析了这两种消息队列和各种不同类型消息的特点,并分析了利用消息驱动任务和子任务的方法.     

Performance analysis of Time Warp with multiple homogeneousprocessors

The behavior of n interacting processors synchronized by the Time Warp protocol is analyzed using a discrete-state, continuous-time Markov chain model. The performance and dynamics of the processes (or processors) are analyzed under the following assumptions: exponential task times and timestamp increments on messages, each event message generates one new message that is sent to a randomly selected process, negligible rollback, state saving, and communication delay, unbounded message buffers, and homogeneous processors. Several performance measures are determined, such as: the fraction of processed events that commit, speedup, rollback probability, expected length of rollback, the probability mass function for the number of uncommitted processed events, the probability distribution function for the virtual time of a process, and the fraction of time the processors remain idle. The analysis is approximate, thus the results have been validated through performance measurements of a Time Warp testbed executing on a shared-memory multiprocessor     

Exploring virtual network selection algorithms in DSM cache coherence protocols

Distributed shared memory (DSM) multiprocessors typically require disjoint networks for deadlock-free execution of cache coherence protocols. This is normally achieved by implementing virtual networks with the help of virtual channels or virtual lanes multiplexed on a single physical network. To keep the coherence protocol simple, messages are usually assigned to virtual lanes in a predefined static manner based on a cycle-free lane assignment dependence graph. However, this static split of virtual networks (such as request and reply networks) may lead to underutilization of certain virtual networks while saturating the other networks. In this paper, we explore different static and dynamic schemes to select the virtual lanes for outgoing messages and mix the load among them without restricting any particular type of message to be carried only by a particular virtual network. We achieve this by exposing the selection algorithms to the coherence protocol itself, so that it can inject messages into selected virtual lanes based on some local information, and still enjoy deadlock-freedom. Our execution-driven simulation on five applications from the SPLASH-2 suite shows that as the system scales, the virtual network selection algorithms play an important role. For 128-node systems, our dynamic selection algorithm speeds up parallel execution by as much as 22 percent over an optimized baseline system running a modified SGI Origin 2000 protocol. We also explore how network latency, the number of message buffers per virtual lane, and the depth of network interface output queues affect the relative performance of various virtual lane selection algorithms.     

Detecting Arbitrary Stable Properties Using Efficient Snapshots

A stable properly continues to hold in an execution once it becomes true. Detecting arbitrary stable properties efficiently in distributed executions is still an open problem. The known algorithms for detecting arbitrary stable properties and snapshot algorithms used to detect such stable properties suffer from drawbacks such as the following: They incur the overhead of a large number of messages per global snapshot, or alter application message headers, or use inhibition, or use the execution history, or assume a strong property such as causal delivery of messages in the system. We solve the problem of detecting an arbitrary stable property efficiently under the following assumptions: P1) the application messages should not be modified, not even by timestamps or message coloring. P2) no inhibition is allowed. P3) the algorithm should not use the message history. P4) any process can initiate the algorithm. This paper proposes a family of nonintrusive algorithms requiring 6(n - 1) control messages, where n is the number of processes. A three-phase strategy of uncoordinated observation of local states is used to give a consistent snapshot from which any stable property can be detected. A key feature of our algorithms is that they do not rely on the processes continually and pessimistically reporting their activity. Only the relevant activity that occurs in the thin slice during the algorithm execution needs to be examined.     

Efficient distributed detection of conjunctions of local predicates

Global predicate detection is a fundamental problem in distributed systems and finds applications in many domains such as testing and debugging distributed programs. This paper presents an efficient distributed algorithm to detect conjunctive-form global predicates in distributed systems. The algorithm detects the first consistent global state that satisfies the predicate even if the predicate is unstable. Unlike previously proposed run-time predicate detection algorithms, our algorithm does not require the exchange of control messages during the normal computation. All the necessary information to detect predicates is piggybacked on computation messages of application programs. The algorithm is distributed because the predicate detection efforts as well as the necessary information are equally distributed among the processes. We prove the correctness of the algorithm and compare its performance with respect to message, storage and computational complexities with that of the previously proposed run-time predicate detection algorithms     

Quantization-based filtering in distributed discrete event simulation

Quantization is an approach to distributed logical simulation in which the value space is quantized and trajectories are represented by the crossings of a set of thresholds. This is an alternative to the common approach which discretizes the time base of a continuous trajectory to obtain a finite number of equally spaced sampled values over time. In distributed simulation, a quantizer checks for threshold crossings whenever an output event occurs and sends this value across to a receiver thereby reducing the number of messages exchanged among federates in a federation. This may increase performance in various ways such as decreasing overall execution time or allowing a larger number of entities to be simulated. Predictive quantization is a more advanced approach that sends just one bit of information instead of the actual real value size with the consequence that not only the number of messages, but also the message size, can be significantly reduced in this approach. In this paper, we present an approach to packaging individual bits into a large message packet, called multiplexed predictive quantization. We demonstrate that this approach can save significant overhead (thereby maximizing data transmission) and can reach close to 100% efficiency in the limit of large numbers of simultaneous message sources encapsulated within individual federates. We also discuss the tradeoff between message bandwidth utilization and the error incurred in the quantization. The results relate bandwidth utilization and error to quantum size for federations executing in the HLA-compliant discrete event distributed simulation environment, DEVS/HLA. The theoretical and empirical results indicate that quantization can be very scaleable due to reduced local computation demands as well as having extremely favorable network load reduction/simulation fidelity tradeoffs.     

A reliable multicast protocol for distributed mobile systems:design and evaluation

Reliable multicast is a powerful communication primitive for structuring distributed programs in which multiple processes must closely cooperate together. We propose a protocol for supporting reliable multicast in a distributed system that includes mobile hosts and evaluate the performance of our proposal through simulation We consider a scenario in which mobile hosts communicate with a wired infrastructure by means of wireless technology. Our proposal provides several novel features. The sender of each multicast may select among three increasingly strong delivery ordering guarantees: FIFO, causal, total. Movements do not trigger the transmission of any message in the wired network as no notion of hand-off is used. The set of senders and receivers (group) may be dynamic. The size of data structures at mobile hosts, the size of message headers, and the number of messages in the wired network for each multicast are all independent of the number of group members. The wireless network is assumed to provide only incomplete spatial coverage and message losses could occur even within cells. Movements are not negotiated and a mobile host that leaves a cell may enter any other cell, perhaps after a potentially long disconnection. The simulation results show that the proposed protocol has good performance and good scalability properties     

Systems of recall broadcast

In a system of recall broadcast, each message contains a set of message identifiers called its recall set. The recall set of a message identifies all previously received messages upon which the message is based. When a message is received by a process and displayed to an external user, all messages in its recall set are also displayed to the user. Our recall broadcast system is efficient in three ways. First, each message is broadcasted only once. Second, each process stores a small number of previously received messages because these messages may be recalled in future messages. Third, processes exchange additional messages to delete previously received messages that can no longer be recalled. The additional messages have the same format as regular messages, and are handled exactly as regular messages.     

Using Forward Reachability Analysis for Verification of Lossy Channel Systems

We consider symbolic on-the-fly verification methods for systems of finite-state machines that communicate by exchanging messages via unbounded and lossy FIFO queues. We propose a novel representation formalism, called simple regular expressions (SREs), for representing sets of states of protocols with lossy FIFO channels. We show that the class of languages representable by SREs is exactly the class of downward closed languages that arise in the analysis of such protocols. We give methods for computing (i) inclusion between SREs, (ii) an SRE representing the set of states reachable by executing a single transition in a system, and (iii) an SRE representing the set of states reachable by an arbitrary number of executions of a control loop. All these operations are rather simple and can be carried out in polynomial time.With these techniques, one can straightforwardly construct an algorithm which explores the set of reachable states of a protocol, in order to check various safety properties. We also show how one can perform model-checking of LTL properties, using a standard automata-theoretic construction. It should be noted that all these methods are by necessity incomplete, even for the class of protocols with lossy channels.To illustrate the applicability of our methods, we have developed a tool prototype and used the tool for automatic verification of (a parameterized version of) the Bounded Retransmission Protocol.     

Analysing a stream authentication protocol using model checking

In this paper, we consider how one can analyse a stream authentication protocol using model checking techniques. In particular, we will be focusing on the Timed Efficient Stream Loss-tolerant Authentication Protocol, TESLA. This protocol differs from the standard class of authentication protocols previously analysed using model checking techniques in the following interesting way: an unbounded stream of messages is broadcast by a sender, making use of an unbounded stream of keys; the authentication of the n-th message in the stream is achieved on receipt of the n+1-th message. We show that, despite the infinite nature of the protocol, it is possible to build a finite model that correctly captures its behaviour.     

A probabilistic approach to estimate the mean waiting times in the earliest deadline first polling

In queueing system, the mean waiting times of messages are important measures to characterize the quality of service (QoS) under various requirements. In a time-critical system, message transactions which cannot meet deadline constraints might lead to catastrophic consequences. Currently, the waiting time estimations using the first-come-first-served (FCFS) and priority (PRI) strategies are already well developed. However, in the case of multi-queue dynamic environments, these quantities are more difficult to analyze due to multiple classes of messages are considered. In this paper, we aim to consider a polling system consisting of a number of parallel infinite-capacity single-server queues. We propose a probabilistic approach to derive the waiting times for different classes of messages by using non-preemptive earliest deadline first (EDF) polling policy. The resulting formula can also lead to the FCFS polling and PRI polling by altering the relative deadlines. Moreover, the bounds of waiting times are discussed. The accuracy of the proposed algorithm is established by comparisons with simulation results. The runtime results are in very good convergence with the theoretical predictions made by our formulas, in terms of prediction accuracies of waiting times and untimely service ratios of messages under various scenarios and timing constraints.