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)

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.

a – Inria
b – Centre de Recherche en Informatique de Nancy (CRIN - CNRS)
1: S4 (INRIA - IRISA)
CNRS : UMR6074 – INRIA – Institut National des Sciences Appliquées (INSA) - Rennes – Université de Rennes 1
2: Institut de recherche en informatique de Toulouse (IRIT)
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

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 detailed 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>