Application of Interface Theories to the Separate Compilation of Synchronous Programs
Résumé
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.
On s'intéresse a la compilation séparée c.- à-d., a la génération 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éré pour un certain bloc sans la connaissance de son contexte (c.- à-d., sans connaître le diagramme dans lequel le bloc est sens être utilisé) et en utilisant un minimum d'information concernant le fonctionnement interne du bloc. La compilation séparée et étudiée par Lublinerman et al. pour le cas particulier des diagrammes mono-horloge, pour lesquels tous les signaux sont mis à jour à partir d'une seule et unique horloge. Dans le même contexte, Pouzet et Raymond ont proposé des algorithmes permettant le passage à l' échelle. L'approche de Lublinerman et al. a été étendue a certaines classes de diagrammes temporels multi-horloges. Dans ce papier, nous étudions le problème en toute généralité et nous montrons qu'il peut être vu comme un problème de synthèse de contrôleur et résolu en utilisant une théorie d'interfaces dite "modale".
Origine : Fichiers produits par l'(les) auteur(s)