Fundamenta Informaticae - Volume 62, issue 2

Authors: Janicki, Ryszard

Article Type: Other

Citation: Fundamenta Informaticae, vol. 62, no. 2, pp. i-ii, 2004

Authors: Bontemps, Yves | Schobbens, Pierre-Yves | Löding, Christof

Article Type: Research Article

Abstract: We propose here Live Sequence Charts with a new, game-based semantics to model interactions between the system and its environment. For constructing programs automatically, we give an algorithm to synthesize either a strategy for the system ensuring that the specification is respected, or, if the specification is unimplementable, a strategy for the environment forcing the system to fail. We introduce the concept of mercifulness, a desirable property of the synthesized program. We give a polynomial time …algorithm for synthesizing merciful winning strategies. Show more

Citation: Fundamenta Informaticae, vol. 62, no. 2, pp. 139-169, 2004

Authors: Cortadella, Jordi | Kondratyev, Alex | Lavagno, Luciano | Taubin, Alexander | Watanabe, Yosinori

Article Type: Research Article

Abstract: This paper presents a synthesis approach for reactive systems that aims at minimizing the overhead introduced by the operating system and the interaction among the concurrent tasks, while considering multiple concurrent execution resources. A formal model based on the notion of scheduling of Petri nets is used to perform the synthesis. We show how the notion of projections of a schedule for the complete system onto the components implemented on separate resources is essential to define …the correctness of the partitioned schedule. Show more

Citation: Fundamenta Informaticae, vol. 62, no. 2, pp. 171-196, 2004

Authors: Esparza, Javier

Article Type: Research Article

Abstract: Signal Transition Graphs (STGs) are one of the most popular models for the specification of asynchronous circuits. A STG can be implemented if it admits a so-called consistent and complete binary encoding. Deciding this is EXPSPACE-hard for arbitrary STGs, and so a lot of attention has been devoted to the subclass of free-choice STGs, which offers a good compromise between expressive power and analizability. In the last years, polynomial time synthesis techniques have been developed for …free-choice STGs, but they assume that the STG has a consistent binary encoding. This paper presents the first polynomial algorithm for checking consistency. Show more

Citation: Fundamenta Informaticae, vol. 62, no. 2, pp. 197-220, 2004

Authors: Khomenko, Victor | Koutny, Maciej | Yakovlev, Alex

Article Type: Research Article

Abstract: The behaviour of asynchronous circuits is often described by Signal Transition Graphs (STGs), which are Petri nets whose transitions are interpreted as rising and falling edges of signals. One of the crucial problems in the synthesis of such circuits is that of identifying whether an STG satisfies the Complete State Coding (CSC) requirement (which states that semantically different reachable states must have different binary encodings), and, if necessary, modifying the STG (by, e.g. inserting new signals …helping to trace the current state) to meet this requirement. This is usually done using reachability graphs. In this paper, we avoid constructing the reachability graph of an STG, which can lead to state space explosion, and instead use only the information about causality and structural conflicts between the events involved in a finite and complete prefix of its unfolding. We propose an efficient algorithm for detection of CSC conflicts based on the Boolean Satisfiability (SAT) approach. Following the basic formulation of the state encoding conflict relationship, we present some problem-specific optimization rules. Experimental results show that this technique leads not only to huge memory savings when compared to the CSC conflicts detection methods based on reachability graphs, but also to significant speedups in many cases. Show more

Keywords: asynchronous circuits, automated synthesis, complete state coding, CSC, Petri nets, signal transition graphs, STG, SAT, net unfoldings, partial order techniques

Citation: Fundamenta Informaticae, vol. 62, no. 2, pp. 221-241, 2004

Authors: Talpin, Jean-Pierre | Le Guernic, Paul | Shukla, Sandeep Kumar | Doucet, Frédéric | Gupta, Rajesh

Article Type: Research Article

Abstract: Rising complexity, increasing performance requirements, and shortening time-to-market demands necessitate newer design paradigms for embedded system design. Such newer design methodologies require raising the level of abstraction for design entry, reuse of intellectual property blocks as virtual components, refinement based design, and formal verification to prove correctness of refinement steps. The problem of combining various components from different designers and companies, designed at different levels of abstraction, and embodying heterogeneous models of …computation is a difficult challenge for the designer community today. Moreover, one of the gating factors for widespread adoption of the system-level design paradigm is the lack of formal models, method and tools to support refinement. In the absence of provably correct and adequate behavioral synthesis techniques, the refinement of a system-level description towards its implementation is primarily a manual process. Furthermore, proving that the implementation preserves the properties of the higher system-level design-abstraction is an outstanding problem. In this paper, we address these issues and define a formal refinement-checking methodology for system-level design. Our methodology is based on a polychronous model of computation of the multi-clocked synchronous formalism SIGNAL. This formalism is implemented in the POLYCHRONY workbench. We demonstrate the effectiveness of our approach by the experimental case study of a SPECC modeling example. First, we define a technique to systematically model SPECC programs in the signal formalism. Second, we define a methodology to compare system-level models of SPECC programs and to validate behavioral equivalence relations between these models at different levels of abstraction. Although we use SPECC modeling examples to illustrate our technique, our methodology is generic and language-independent and the model that supports it conceptually minimal by offering a scalable notion and a flexible degree of abstraction. Show more

Citation: Fundamenta Informaticae, vol. 62, no. 2, pp. 243-273, 2004