Validation of Mixed Signal-Alpha Real-Time Systems through Affine Calculus on Clock Synchronisation Constraints
| Autor: | Thierry Gautier, Irina M. Smarandache, Paul Le Guernic |
|---|---|
| Přispěvatelé: | Parallel algorithms and load sharing (APACHE), Informatique et Distribution (ID-IMAG), Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National Polytechnique de Grenoble (INPG)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National Polytechnique de Grenoble (INPG)-Centre National de la Recherche Scientifique (CNRS)-Inria Grenoble - Rhône-Alpes, Institut National de Recherche en Informatique et en Automatique (Inria)-Université Joseph Fourier - Grenoble 1 (UJF), Distributed Systems for Cooperative Applications (SIRAC), Inria Grenoble - Rhône-Alpes, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Environnement de programmation d'applications temps réel (EP-ATR), 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, Institut National de Recherche en Informatique et en Automatique (Inria), 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 |
| Jazyk: | angličtina |
| Rok vydání: | 1999 |
| Předmět: |
Theoretical computer science
Computer science Real-time computing 020207 software engineering Mixed-signal integrated circuit 02 engineering and technology computer.software_genre Synchronization 020202 computer hardware & architecture 0202 electrical engineering electronic engineering information engineering Calculus Systems design [INFO.INFO-ES]Computer Science [cs]/Embedded Systems Compiler Affine transformation Formal verification Algorithm computer Real-time operating system |
| Zdroj: | FM'99-Formal Methods, World Congress on Formal Methods in the Development of Computing Systems World Congress on Formal Methods in the Development of Computing Systems (FM'99) World Congress on Formal Methods in the Development of Computing Systems (FM'99), Sep 1999, Toulouse, France. pp.1364-1383, ⟨10.1007/3-540-48118-4_22⟩ FM’99 — Formal Methods ISBN: 9783540665885 World Congress on Formal Methods |
| DOI: | 10.1007/3-540-48118-4_22⟩ |
| Popis: | International audience; In this paper we present the affine clock calculus as an extension of the formal verification techniques provided by the SIGNAL language. A SIGNAL program describes a system of clock synchronisation constraints the consistency of which is verified by compilation (clock calculus). Well-adapted in control-based system design, the clock calculus has to be extended in order to enable the validation of SIGNAL-ALPHA applications which usually contain important numerical calculations. The new affine clock calculus is based on the properties of affine relations induced between clocks by the refinement of SIGNAL-ALPHA specifications in a codesign context. Affine relations enable the derivation of a new set of synchronisability rules which represent conditions against which synchronisation constraints on clocks can be assessed. Properties of affine relations and synchronisability rules are derived in the semantical model of traces of SIGNAL. A prototype implementing a subset of the synchronisability rules has been integrated in the SIGNAL compiler and used for the validation of a video image coding application specified using SIGNAL and ALPHA. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|