Application of Interface Theories to the Separate Compilation of Synchronous Programs

Albert Benveniste; Caillaud Benoît; Raclet Jean-Baptiste

hal-00721049, version 1

Application of Interface Theories to the Separate Compilation of Synchronous Programs

Albert Benveniste (, ) ¹, Caillaud Benoît (, )^a^, 1, Raclet Jean-Baptiste (, )^b^, 2

N° RR-8030 (2012)

a – Inria
b – Centre de Recherche en Informatique de Nancy (CRIN - CNRS)
1: S4 (INRIA - IRISA)
http://www.inria.fr/equipes/s4
CNRS : UMR6074 – INRIA – Institut National des Sciences Appliquées (INSA) - Rennes – Université de Rennes 1 Campus de Beaulieu 35042 Rennes cedex France
2: Institut de recherche en informatique de Toulouse (IRIT)
http://www.irit.fr/
CNRS : UMR5505 – Institut National Polytechnique de Toulouse - INPT – Université des Sciences Sociales - Toulouse I – Université Toulouse I [UT1] Capitole – Université Toulouse le Mirail - Toulouse II – Université Paul Sabatier [UPS] - Toulouse III 118 Route de Narbonne, F-31062 Toulouse Cedex 9 France

Bibliographic reference

Type of document: Research reports
Domain: Computer Science/Embedded Systems
Title: Application of Interface Theories to the Separate Compilation of Synchronous Programs
Abstract: We study the problem of separate compilation, i.e., the generation of modular code, for the discrete time part of block-diagrams formalisms such as Simulink, Modelica, or Scade. Code is modular in that it is generated for a given composite block independently from context (i.e., without knowing in which diagrams the block is to be used) and using minimal information about the internals of the block. Just using o -the-shelf C code generation (e.g., as available in Simulink) does not provide modular code. Separate compilation was solved by Lublinerman et al. for the special case of single-clocked diagrams, in which all signals are updated at a same unique clock. For the same case, Pouzet and Raymond proposed algorithms that scale-up properly to real-size applications. The technique of Lublinerman et al. was extended to some classes of multi-clocked and timed diagrams. We study this problem in its full generality and we show that it can be cast to a special class of controller synthesis problems by relying on recently proposed modal interface theories.
Abstract in french: On s'int eresse a la compilation s epar ee c.- a-d., a la g en eration de code modulaire, pour le sous-ensemble discret des formalismes de diagrammes de bloc tels que Simulink, Modelica ou Scade. Un code est modulaire lorsqu'il est g en er e pour un certain bloc sans la connaissance de son contexte (c.- a-d., sans conna^ tre le diagramme dans lequel le bloc est sens e ^etre utilis e) et en utilisant un minimum d'information concernant le fonctionnement interne du bloc. La compilation s epar ee a et e etudi ee par Lublinerman et al. pour le cas particulier des diagrammes mono-horloge, pour lesquels tous les signaux sont mis a jour a partir d'une seule et unique horloge. Dans le m^eme contexte, Pouzet et Raymond ont propos e des algorithmes permettant le passage a l' echelle. L'approche de Lublinerman et al. a et e etendue a certaines classes de diagrammes temporels multi-horloges. Dans ce papier, nous etudions le probl eme en toute g en eralit e et nous montrons qu'il peut ^etre vu comme un probl eme de synth ese de contr^oleur et r esolu en utilisant une th eorie d'interfaces dite \modale".
ACM Classification: D.: Software
Full text language: English
Report type: Research Report
Publication date: 2012-07-26
Keywords: compilation – synchronous program – component-based design – compositional reasoning – interface theories – modal speci cations
Writing date: 2012-07-26
Internal note: RR-8030

Attached file list to this document:

TEX

(1.2 KB)

(14.9 KB)

(11.1 KB)

(5.3 KB)

(1.5 KB)

(3.1 KB)

(1.6 KB)

(6.1 KB)

(1.4 KB)

(3.8 KB)

(1.5 KB)

(4.4 KB)

(1.5 KB)

(4.7 KB)

(1.5 KB)

(5.9 KB)

(2.3 KB)

(5.6 KB)

(1.3 KB)

(7.1 KB)

(1.4 KB)

(5.5 KB)

(1.1 KB)

(6.6 KB)

(1.7 KB)

(15.3 KB)

(815.3 KB)

(815.2 KB)

(45.9 KB)

SeparateCompilFinal.pdf

(258.3 KB)

SeparateCompilFinalAlbert.pdf

(362.1 KB)

(4.6 KB)

(891 B)

(2.8 MB)

(47.6 KB)

(367.9 KB)

(5.4 MB)

PDF

RR-8030.pdf

(526 KB)

hal-00721049, version 1
http://hal.inria.fr/hal-00721049
oai:hal.inria.fr:hal-00721049
From: Albert Benveniste <>
Submitted on: Thursday, 26 July 2012 14:35:15
Updated on: Monday, 30 July 2012 10:51:21

See short view

Associated documents

PDF :

Export

Bibtex EndNote TEI RefWorks

%F hal-00721049, version 1
%0 Report
%U http://hal.inria.fr/hal-00721049
%2 INFO:INFO_ES
%T Application of Interface Theories to the Separate Compilation of Synchronous Programs
%A Benveniste, Albert
%A Benoît, Caillaud
%A Jean-Baptiste, Raclet
%+ S4 - INRIA - IRISA , Institut de recherche en informatique de Toulouse - IRIT
%Z S4, IRIT
%X We study the problem of separate compilation, i.e., the generation of modular code, for the discrete time part of block-diagrams formalisms such as Simulink, Modelica, or Scade. Code is modular in that it is generated for a given composite block independently from context (i.e., without knowing in which diagrams the block is to be used) and using minimal information about the internals of the block. Just using o -the-shelf C code generation (e.g., as available in Simulink) does not provide modular code. Separate compilation was solved by Lublinerman et al. for the special case of single-clocked diagrams, in which all signals are updated at a same unique clock. For the same case, Pouzet and Raymond proposed algorithms that scale-up properly to real-size applications. The technique of Lublinerman et al. was extended to some classes of multi-clocked and timed diagrams. We study this problem in its full generality and we show that it can be cast to a special class of controller synthesis problems by relying on recently proposed modal interface theories.
%2 On s'int eresse a la compilation s epar ee c.- a-d., a la g en eration de code modulaire, pour le sous-ensemble discret des formalismes de diagrammes de bloc tels que Simulink, Modelica ou Scade. Un code est modulaire lorsqu'il est g en er e pour un certain bloc sans la connaissance de son contexte (c.- a-d., sans conna^ tre le diagramme dans lequel le bloc est sens e ^etre utilis e) et en utilisant un minimum d'information concernant le fonctionnement interne du bloc. La compilation s epar ee a et e etudi ee par Lublinerman et al. pour le cas particulier des diagrammes mono-horloge, pour lesquels tous les signaux sont mis a jour a partir d'une seule et unique horloge. Dans le m^eme contexte, Pouzet et Raymond ont propos e des algorithmes permettant le passage a l' echelle. L'approche de Lublinerman et al. a et e etendue a certaines classes de diagrammes temporels multi-horloges. Dans ce papier, nous etudions le probl eme en toute g en eralit e et nous montrons qu'il peut ^etre vu comme un probl eme de synth ese de contr^oleur et r esolu en utilisant une th eorie d'interfaces dite \modale".
%2 D.: Software
%G English
%2 Research Report
%8 2012-07-26
%K compilation; synchronous program; component-based design; compositional reasoning; interface theories; modal speci cations
%2 2012-07-26
%Z RR-8030

<?xml version="1.0" encoding="UTF-8"?>
<listBibl xmlns="http://www.tei-c.org/ns/1.0" xmlns:xlink="http://www.w3.org/1999/xlink" xmlns:mml="http://www.w3.org/1998/Math/MathML">
<listBibl type="report"><head>Research reports</head>
<biblStruct type="report" xml:id="hal-00721049"><monogr>
<author><persName><forename>Albert</forename><surname>Benveniste</surname></persName>
<affiliation>
<orgName type="laboratory">INRIA - IRISA</orgName>
<orgName type="team">S4</orgName>
<country>FR</country>
<orgName type="institution">CNRS : UMR6074</orgName>
<orgName type="institution">INRIA</orgName>
<orgName type="institution">Institut National des Sciences Appliquées (INSA) - Rennes</orgName>
<orgName type="institution">Université de Rennes 1</orgName>
</affiliation>
</author>
<author><persName><forename>Caillaud</forename><surname>Benoît</surname></persName>
<affiliation>
<orgName type="laboratory">INRIA - IRISA</orgName>
<orgName type="team">S4</orgName>
<country>FR</country>
<orgName type="institution">CNRS : UMR6074</orgName>
<orgName type="institution">INRIA</orgName>
<orgName type="institution">Institut National des Sciences Appliquées (INSA) - Rennes</orgName>
<orgName type="institution">Université de Rennes 1</orgName>
</affiliation>
</author>
<author><persName><forename>Raclet</forename><surname>Jean-Baptiste</surname></persName>
<affiliation>
<orgName type="laboratory">IRIT</orgName>
<orgName type="team">Institut de recherche en informatique de Toulouse</orgName>
<country>FR</country>
<orgName type="institution">CNRS : UMR5505</orgName>
<orgName type="institution">Institut National Polytechnique de Toulouse - INPT</orgName>
<orgName type="institution">Université des Sciences Sociales - Toulouse I</orgName>
<orgName type="institution">Université Toulouse I [UT1] Capitole</orgName>
<orgName type="institution">Université Toulouse le Mirail - Toulouse II</orgName>
<orgName type="institution">Université Paul Sabatier [UPS] - Toulouse III</orgName>
</affiliation>
</author>
<title type="main" level="m">Application of Interface Theories to the Separate Compilation of Synchronous Programs</title><title type="main" level="m">Application of Interface Theories to the Separate Compilation of Synchronous Programs</title><imprint><biblScope type="publicationDate">2012-07-26</biblScope></imprint></monogr><idno type="HALid">http://hal.inria.fr/hal-00721049</idno><idno type="HALFile">http://hal.inria.fr/hal-00721049/PDF/RR-8030.pdf</idno></biblStruct>
</listBibl>
</listBibl>