1. Formal Refinement Checking in a System-level Design Methodology
- Author
-
Talpin, Jean-Pierre, Le Guernic, Paul, Shukla, Sandeep, Doucet, Frédéric, Gupta, R.K., Synchronous programming for the trusted component-based engineering of embedded systems and mission-critical systems (ESPRESSO), Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), Université de Rennes 1 (UR1), Université de Rennes (UNIV-RENNES)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Rennes 1 (UR1), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Inria Rennes – Bretagne Atlantique, Institut National de Recherche en Informatique et en Automatique (Inria), FERMAT Lab, Department of Electrical and Computer Engineering [Blacksburg] (ECE), Virginia Tech [Blacksburg]-Virginia Tech [Blacksburg], Department of Computer Science and Engineering [San Diego] (CSE-UCSD), University of California [San Diego] (UC San Diego), University of California-University of California, Université de Rennes (UR)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Rennes (UR)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Inria Rennes – Bretagne Atlantique, Department of Computer Science and Engineering [Univ California San Diego] (CSE - UC San Diego), and University of California (UC)-University of California (UC)
- Subjects
[INFO.INFO-ES]Computer Science [cs]/Embedded Systems - Abstract
International audience; 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.
- Published
- 2004