Search

Asynchronous automata are parallel compositions of finite-state processes synchronizing over shared variables. A deep theorem due to Zielonka says that every regular trace language can be represented by a deterministic asynchronous automaton. In this paper we improve the construction, in that the size of the obtained asynchronous automaton is polynomial in the size of a given DFA and simply exponential in the number of processes. We show that our construction is optimal within the class of automata produced by Zielonka-type constructions. In particular, we provide the first non trivial lower bound on the size of asynchronous automata. [ABSTRACT FROM AUTHOR]

With more and more data stored into XML databases, there is a need to provide the same level of failure resilience and robustness that users have come to expect from relational database systems. In this work, we discuss strategies to provide the transactional aspect of atomicity to XML databases. The main contribution of this paper is to propose a novel approach for performing updates-in-place on XML databases, with the undo statements stored in the same high level language as the update statements. Finally, we give experimental results to study the performance/storage trade-off of the updates-in-place strategy (based on our undo proposal) against the deferred updates strategy to providing atomicity. [ABSTRACT FROM AUTHOR]

Good scheduling policies for distributed embedded applications are required for meeting hard real time constraints and for optimizing the use of computational resources. We study the quasi-static scheduling problem in which (uncontrollable) control flow branchings can influence scheduling decisions at run time. Our abstracted task model consists of a network of sequential processes that communicate via point-to-point buffers. In each round, the task gets activated by a request from the environment. When the task has finished computing the required responses, it reaches a pre-determined configuration and is ready to receive a new request from the environment. For such systems, we prove that determining existence of quasi-static scheduling policies is undecidable. However, we show that the problem is decidable for the important sub-class of ˵data branching″ systems in which control flow branchings are due exclusively to data-dependent internal choices made by the sequential components. This decidability result–which is non-trivial to establish–exploits ideas derived from the Karp and Miller coverability tree [8] as well as the existential boundedness notion of languages of message sequence charts [6]. [ABSTRACT FROM AUTHOR]

Classical verification often uses abstraction when dealing with data. On the other hand, dynamic XML-based applications have become pervasive, for instance with the ever growing importance of web services. We define here Tree Pattern Rewriting Systems (TPRS) as an abstract model of dynamic XML-based documents. TPRS systems generate infinite transition systems, where states are unranked and unordered trees (hence possibly modeling XML documents). Their guarded transition rules are described by means of tree patterns. Our main result is that given a TPRS system ]> , a tree pattern P and some integer k such that any reachable document from T has depth at most k, it is decidable (albeit of non elementary complexity) whether some tree matching P is reachable from T. [ABSTRACT FROM AUTHOR]

An effective way to assemble partial views of a distributed system is to compute their product. Given two Message Sequence Graphs, we address the problem of computing a Message Sequence Graph that generates the product of their languages, when possible. Since all MSCs generated by a Message Sequence Graph G may be run within fixed bounds on the message channels (that is, G is existentially bounded), a subproblem is to decide whether the considered product is existentially bounded. We show that this question is undecidable, but turns co-NP-complete in the restricted case where all synchronizations belong to the same process. This is the first positive result on the decision of existential boundedness. We propose sufficient conditions under which a Message Sequence Graph representing the product can be constructed. [ABSTRACT FROM AUTHOR]

The analysis of message sequence charts (MSCs) is highly important in preventing common problems in communication protocols. Detecting race conditions, i.e., possible discrepancies in event order, was studied for a single MSC and for MSC graphs (a graph where each node consists of a single MSC, also called HMSC). For the former case, this problem can be solved in quadratic time, while for the latter case it was shown to be undecidable. However, the prevailing real-life situation is that a collection of MSCs, called here an ensemble, describing the different possible scenarios of the system behavior, is provided, rather than a single MSC or an MSC graph. For an ensemble of MSCs, a potential race condition in one of its MSCs can be compensated by another MSC in which the events occur in a different order. We provide a polynomial algorithm for detecting races in an ensemble. On the other hand, we show that in order to prevent races, the size of an ensemble may have to grow exponentially with the number of messages. Also, we initiate the formal study of the standard MSC coregion construct, which is used to relax the order among events of a process. We show that by using this construct, we can provide more compact race-free ensembles; however, detecting races becomes NP-complete. [ABSTRACT FROM AUTHOR]

Scenario languages based on Message Sequence Charts (MSCs) and related notations have been widely studied in the last decade [14,13,2,9,6,12,8]. The high expressive power of scenarios renders many basic problems concerning these languages undecidable. The most expressive class for which several problems are known to be decidable is one which possesses a behavioral property called "existentially bounded". However, scenarios outside this class are frequently exhibited by asynchronous distributed systems such as sliding window protocols. We propose here an extension of MSCs called Causal Message Sequence Charts, which preserves decidability without requiring existential bounds. Interestingly, it can also model scenarios from sliding window protocols. We establish the expressive power and complexity of decision procedures for various subclasses of Causal Message Sequence Charts. [ABSTRACT FROM AUTHOR]

The well-known algorithm of Zielonka describes how to transform automatically a sequential automaton into a deterministic asynchronous trace automaton. In this paper, we improve the construction of deterministic asynchronous automata from finite state automaton. Our construction improves the well-known construction in that the size of the asynchronous automaton is simply exponential in both the size of the sequential automaton and the number of processes. In contrast, Zielonka’s algorithm gives an asynchronous automaton that is doubly exponential in the number of processes (and simply exponential in the size of the automaton). [ABSTRACT FROM AUTHOR]

There are many cases where we want to verify a system that does not have a usable formal model: the model may be missing, out of date, or simply too big to be used. A possible method is to analyze the system while learning the model (black box checking). However, learning may be an expensive task, thus it needs to be guided, e.g., using the checked property or an inaccurate model (adaptive model checking). In this paper, we consider the case where some of the system components are completely specified (white boxes), while others are unknown (black boxes), giving rise to a grey box system. We provide algorithms and lower bounds, as well as experimental results for this model. [ABSTRACT FROM AUTHOR]

The classical modelization of concurrent system behaviors is based on observing execution sequences of global states. This model is intuitively simple and enjoys a variety of mathematical tools, e.g. finite automata, helping verifying concurrent systems. On the other hand, parallel composition of local controllers are needed when dealing with the actual implementation of concurrent models. A well known tool for turning global observation into local controllers is Zielonka's theorem, and its derivatives. We give here another algorithm, simpler and cheaper than Zielonka's theorem, in the case where the events observed do not include communication but only local asynchronous actions. In a developer point of view, it means that she does not have to explicitly specify the messages needed, which will be added (if allowed) automatically by the implementation algorithm. [ABSTRACT FROM AUTHOR]

The classical model for concurrent systems is based on observing execution sequences of global states, separated from each other by atomic transitions. This model is intuitively simple and enjoys a variety of mathematical tools, e.g., finite automata and linear temporal logic, and algorithms that can be applied in order to test and verify concurrent systems. Although this model is sufficient for most frequently used validation tasks, some phenomena of concurrent systems are difficult to express using its related formalisms. In particular, not all the global states (snapshots) related to an execution appear on a particular execution sequence; some appear on equivalent sequences. Previous attempts to move into formalisms that are based on a more detailed model of execution, e.g,. the causality based model, resulted in specification formalisms with inherently high complexity verification algorithms. We study here verification problems that involve allowing the execution sequences model to observe past global states from equivalent executions. We show various algorithms and complexity results related to our extension of the interleaving model. [ABSTRACT FROM AUTHOR]

Communicating Finite States Machines (CFMs) and Message Sequence Graphs (MSC-graphs for short) are two popular specification formalisms for communicating systems. MSC-graphs capture requirements (scenarios), hence they are the starting point of the design process. Implementing an MSC-graph means obtaining an equivalent deadlock-free CFM, since CFMs correspond to distributed message-passing algorithms. Several partial answers for the implementation have been proposed. E.g., local-choice MSC-graphs form a subclass of deadlock-free CFM: Testing equivalence with some local-choice MSC-graph is thus a partial answer to the implementation problem. Using Compositional MSCs, we propose a new algorithm which captures more implementable models than with MSCs. Furthermore, the size of the implementation is reduced by one exponential. [ABSTRACT FROM AUTHOR]