Fundamenta Informaticae

Resynthesis of handshake specifications obtained e.g. from BALSA or TANGRAM with speed-independent logic synthesis from STGs is a promising approach. To deal with state-space explosion,we suggested STG decomposition; a problemis that decomposition can lead to irreducible CSC conflicts.

Here, we present a new approach to solve such conflicts by introducing internal communication between the components. We give some first, very encouraging results for very large STGs concerning synthesis time and circuit area.

This paper introduces enhancements to the synthesis of circuits that involve write-afterread (WAR) operations and use the four-phase handshake protocol. The paper demonstrates that the use of edge-triggering makes possible many useful trade-offs among speed, area and powerdelay product. Significant increases in speed are possible as a result of increased concurrency in the circuit's operation, which compensates for much of the penalty associated with the down phase of the four-phase protocol. It is also shown that concurrency can be increased by the judicious insertion of T-elements in the system's control structure. Simulation results for a 16-bit accumulator showed a speed increase of 50% and a reduction of 23% in the power-delay product. The speed of a radix-4 Booth multiplier increased by over 27% and its area and energy consumption were reduced by 5%. These results were derived using test circuits synthesized by Balsa and implemented in Synopsys using 180-nm technology.

A Token-ManagedAdmission Control (TMAC) mechanism is introduced in order to provide efficient Quality-of-Service (QoS) support for different types of application on a best-effort Globally-Asynchronous Locally-Synchronous (GALS) interconnect fabric. The mechanism is applied at the ingress edges of the fabric using tokens to allocate dynamic network resources and prevent network congestion. The degree of fairness is controllable, in order to balance the desired throughput and data transfer resource allocation appropriately for a particular application. The simulation and analysis presented here shows efficient QoS provision. Our detailed implementation and analysis show that TMAC provides service guarantees on the network while using a modest physical area because of the simplicity of the control logic.

Service Oriented Computing (SOC) allows for the composition of services which communicate using unidirectional one-way or bidirectional request-response communication patterns. Most service orchestration languages proposed so far provide also primitives for error handling based on fault, termination, and compensation handlers. Our work is motivated by the difficulties encountered in programming some error handling strategies using current error handling primitives. We propose as a solution an orchestration programming style in which handlers are dynamically installed. We assess our proposal by formalizing our approach as an extension of the process calculus SOCK and by proving that our formalization satisfies some expected high-level properties.

Assuring Quality of Service (QoS) properties is critical in Service-Oriented Application (SOA) development. In this paper, we present an approach for specifying the QoS properties of services along multiple dimensions and selecting services for their composition in a way that optimizes the QoS of the result. We apply the integration of concerns paradigm to allow combined specification of QoS and functional properties by using Quantitative Constraint Automata, which integrate QoS aspects into service-oriented application development processes, mainly for service selection and composition.

The design of complex concurrent systems often involves intricate performance and dependability considerations. Continuous-time Markov chains (CTMCs) are a widely used modeling formalism that captures such performance and dependability properties, and makes them analyzable by model checking. In this paper, we focus on time-bounded probabilistic properties of infinite-state CTMCs, expressible in a subset of continuous stochastic logic (CSL). This comprises important dependability measures, such as time-bounded probabilistic reachability, performability, survivability, and various availability measures like instantaneous, conditional instantaneous and interval availabilities. Conventional model checkers explore the given model exhaustively, which is often costly, due to state explosion, and sometimes impossible because the model is infinite. This paper presents a method that only explores the model up to a finite depth. The required depth is determined on the fly by an algorithm that is configurable in order to adapt to the characteristics of different classes of models. We provide experimental evidence showing that our method is effective.

We present a process-algebraic framework for performance evaluation of discrete-time discrete-event systems. The modeling of the system builds on a process algebra with conditionallydistributed discrete-time delays and generally-distributed stochastic delays. In the general case, the performance analysis is done with the toolset of the modeling language χ by means of discrete-event simulation. The process-algebraic setting allows for expansion laws for the parallel composition and the maximal progress operator, so one can directly manipulate the process terms and transform the specification in a required form. This approach is illustrated by specifying and solving the recursive specification of the G/G/1/∞ queue, as well as by specifying a variant of the concurrent alternating bit protocol with generally-distributed unreliable channels. In a specific situation when all delays are assumed deterministic, we turn to performance analysis of probabilistic timed systems. This work employs discrete-time probabilistic reward graphs, which comprise deterministic delays and immediate probabilistic choices. Here, we extend previous investigations on the topic, which only touched long-run analysis, to tackle transient analysis as well. The theoretical results obtained allow us to extend the χ-toolset. For illustrative purposes, we analyze the concurrent alternating bit protocol in the extended environment of the χ-toolset using discrete-event simulation for generallydistributed channels, the developed analytical method for deterministic channels, and Markovian analysis for exponentially-distributed delays.

In this paper we present an algorithm to synthesize a finite unlabelled place/transition Petri net (p/t-net) from a possibly infinite partial language, which is given by a term over a finite set of labelled partial orders using operators for union, iteration, parallel composition and sequential composition. The synthesis algorithm is based on the theory of regions for partial languages presented in [17] and produces a p/t-net having minimal net behaviour including the given partial language. The algorithm uses linear programming techniques that were already successfully applied in [22] for the synthesis of p/t-nets from finite partial languages. Also, an equality test algorithm to check whether the behaviour of the synthesized p/t-net equals the given partial language is shown. Moreover, we present an implementation of the developed synthesis algorithm together with an example case study. Finally, a possible generalization of the presented term based representation of infinite partial languages is discussed.

This paper considers distributed systems, defined as a collection of components interacting through interfaces. Components, interfaces and distributed systems are modeled as Petri nets. It is well known that the unfolding of such a distributed system factorises, in the sense that it can be expressed as the composition of unfoldings of its components. This factorised form of the unfolding generally provides a more compact representation of the system runs, because each component does not need to represent the possible choices (conflicts) appearing in the other components. Moreover, the unfolding factorisation makes it possible to analyse the system by parts.

The paper focuses on the derivation of a finite and complete prefix (FCP) in the unfolding of a distributed system. Specifically, one would like to directly obtain such a FCP in factorised form, without computing first a FCP of the global distributed system and then factorising it. The construction of such a "modular FCP" is based on deriving summaries of component behaviours w.r.t. their interfaces, that are then communicated to the neighbouring components. The latter combine these summaries with their local behaviours, and prepare interface summaries for the next components. This globally takes the form of a message passing algorithm, where the global system is never considered.