Fundamenta Informaticae - Volume 78, issue 1

Article Type: Other

Citation: Fundamenta Informaticae, vol. 78, no. 1, pp. i-ii, 2007

Authors: Clarisó, Robert | Cortadella, Jordi

Article Type: Research Article

Abstract: A technique for the verification of concurrent parametric timed systems is presented. In the systems under study, each action has a bounded delay where the bounds are either constants or parameters. Given a safety property, the analysis computes automatically a set of constraints on the parameters that is sufficient to guarantee the property. The main contribution is an innovative representation of the parametric timed state space based on bit-vectors. Experimental results from the domain of timed …circuits show that this representation improves the efficiency of the verification significantly with a small impact on the accuracy of the derived constraints. Show more

Keywords: Formal Verification, Abstract Interpretation, Parametric Timed Systems

Citation: Fundamenta Informaticae, vol. 78, no. 1, pp. 1-33, 2007

Authors: Geilen, Marc | Basten, Twan | Theelen, Bart | Otten, Ralph

Article Type: Research Article

Abstract: Multi-criteria optimisation problems occur naturally in many engineering practices. Pareto analysis has proven to be a powerful tool to characterise potentially interesting realisations of a particular engineering problem. It is therefore used frequently for design-space exploration problems. Depending on the optimisation goals, one of the Pareto-optimal alternatives will be the optimal realisation. It often happens however, that partial design decisions have to be taken, leaving other aspects of the optimisation problem to …be decided at a later stage, and that Pareto-optimal configurations have to be composed (dynamically) from Pareto-optimal configurations of components. These aspects are not supported by current analysis methods. This paper introduces a novel, algebraic approach to Pareto analysis. The approach is particularly designed to allow for describing incremental design decisions and composing sets of Pareto-optimal configurations. The algebra can be used to study the operations on Pareto sets and the efficient computation of Pareto sets and their compositions. The algebra is illustrated with a case-study based on transmitting an MPEG-4 video stream from a server to a hand-held device. Show more

Citation: Fundamenta Informaticae, vol. 78, no. 1, pp. 35-74, 2007

Authors: Gorgônio, Kyller | Cortadella, Jordi | Xia, Fei | Yakovlev, Alex

Article Type: Research Article

Abstract: Asynchronous data communication mechanisms (ACMs) have been extensively studied as data connectors between independently timed processes in digital systems. In previous work, systematic ACM synthesis methods have been proposed. In this paper, we advance this work by developing algorithms and software tools which automate most of the ACM synthesis process. Firstly, an interleaving specification is constructed in the form of a state graph, and secondly, a Petri net model of an "ACM-type" is …derived using the theory of regions. The method is applied to a number of "standard" writing and reading policies of ACMs with shared memory and unidirectional control variables. Show more

Keywords: Asynchronous communicationmechanisms, Petri nets, concurrent and distributed systems, embedded systems, hardware and software codesign, protocols, synthesis

Citation: Fundamenta Informaticae, vol. 78, no. 1, pp. 75-100, 2007

Authors: Josephs, Mark B. | Kapoor, Hemangee K.

Article Type: Research Article

Abstract: Josephs and Udding's DI-Algebra offers a convenient way of specifying and verifying designs that must rely upon delay-insensitive signalling between modules (asynchronous logic blocks). It is based on Hoare's theory of CSP, including the notion of refinement between processes, and is similarly underpinned by a denotational semantics. Verhoeff developed an alternative theory of delay-insensitive design based on a testing paradigm and the concept of reflection. The first contribution of this paper is …to define a relation between processes in DI-Algebra that captures Verhoeff's notion of a closed system passing a test (by being free of interference and deadlock). The second contribution is to introduce a new notion of controllability, that is, to define what it means for a process to be controllable in DI-Algebra. The third contribution is to extend DI-Algebra with a reflection operator and to show how testing relates to controllability, reflection and refinement. It is also shown that double reflection yields fully-abstract processes in the sense that it removes irrelevant distinctions between controllable processes. The final contribution is a modified version of Verhoeff's factorisation theorem that could potentially be of major importance for constructive design and the development of design tools. Several elementary examples are worked out in detail to illustrate the concepts. The claims made in this paper are accompanied by formal proofs, mostly in an annotated calculational style. Show more

Keywords: Process algebra, refinement, testing, controllability, reflection, factorisation

Citation: Fundamenta Informaticae, vol. 78, no. 1, pp. 101-130, 2007

Authors: Potop-Butucaru, Dumitru | Caillaud, Benoît

Article Type: Research Article

Abstract: In this paper, we introduce a new model for the representation of distributed asynchronous implementations of synchronous specifications. The model covers classical implementations, where a notion of global synchronization is preserved by means of signaling, and globally asynchronous, locally synchronous (GALS) implementations where the global clock is removed. The new model offers a unified framework for reasoning about two essential correctness properties of an implementation: the preservation of semantics and the absence of deadlocks. We …use it to derive criteria ensuring the correct deployment of synchronous specifications over GALS architectures. As the model captures the internal concurrency of the synchronous specification, our criteria support implementations that are less constrained and more efficient than existing ones. Our work also reveals strong ties between abstract semantics-preservation properties and more operational ones like the absence of deadlocks. Show more

Keywords: Synchronous systems, Asynchronous systems, Globally asynchronous, locally synchronous (GALS) architectures, Kahn processes, Endochronous systems, Semantics preservation

Citation: Fundamenta Informaticae, vol. 78, no. 1, pp. 131-159, 2007

Authors: Vogler, W. | , B. | Kangsah,

Article Type: Research Article

Abstract: Signal Transition Graphs (STGs) are a version of Petri nets for the specification of asynchronous circuit behaviour. It has been suggested to decompose such a specification as a first step; this leads to a modular implementation, which can support circuit synthesis by possibly avoiding state explosion or allowing the use of library elements. In a previous paper, the originalmethod was extended and shown to bemuchmore generally applicable than known before. But further extensions are necessary, …and some are presented in this paper. In particular, to avoid dynamic auto-conflicts, the previous paper insisted on avoiding structural autoconflicts, which is too restrictive; as a main contribution, we show how to work with the latter type of auto-conflicts. This extension makes it necessary to restructure presentation and correctness proof of the decomposition algorithm. Show more

Keywords: concurrent systems, Petri nets, asynchronous circuits, Signal Transition Graphs, decomposition, modular implementation, state explosion

Citation: Fundamenta Informaticae, vol. 78, no. 1, pp. 161-197, 2007