Publications 1998

J.R. Beauvais, R. Houdebine, P. Le Guernic, E. Rutten, T. Gautier.
A translation of Statecharts and Activitycharts into Signal equations.  Rapport de Recherche Irisa / Inria-Rennes, No3397, Avril 1998. (postscript)
Résumé : The languages for modeling reactive systems can be divided in two styles: the imperative, state-based ones and the declarative, data-flow ones. Each of them is best adapted to a given application domain. This paper, through the example of the languages Statecharts and Signal, shows a way to translate an imperative specification (Statecharts) to a declarative, equational one (Signal). This translation makes multi-formalism specification possible, and provides a support for the interoperability of the languages. It gives access from a Statecharts specification to the DC+ exchange format between the tools implementing the synchronous technology, using e.g. the clock calculus available in Signal. Statecharts specifications can thereby be applied functionalities of verification, validation, compilation, optimization, efficient and compact code generation, distributed and execution architecture-dependent code generation. The results presented here cover the essential features of StateCharts as well as of another language of Statemate: Activitycharts.
Keywords: Signal, Statecharts, Activitycharts, DC+, reactive & real-time systems, synchronous languages, interoperability, code generation

A. Benveniste, (AVECM. Siegel, L. Holenderski, K. Winkelmann, E. Sefton, E. Rutten, P. Le Guernic, T. Gautier).
Safety Critical Embedded Systems Design: the SACRES approach.  Formal Techniques in Real-Time and Fault Tolerant systems, FTRTFT'98 school, Lyngby, Denmark, Septembre 1998. (postscript)
Résumé : The SACRES project is an Esprit R&D project, SACRES members are: Siemens (Lead partner), i-Logix, TNI (Techniques Nouvelles d'Informatique), OFFIS, INRIA, the Weizmann Institute of Science, British Aerospace, SNECMA. As its name indicates, SACRES is dealing with the development of new design methodologies and associated tools for safety critical embedded systems. Main targeted users are aeronautics, automobile, process control and energy. Emphasis has been put on formal techniques for modular verification of the specifications, distributed code generation, and generated code validation against specifications. These techniques aim at making more flexible the exploration of the software life cycle. Verification of the specifications and generated code validation aim at helping for certification of the overall design. Distributed code generation aims at reducing the dependency of the design with respect to the target supporting architecture. In all cases, modularity helps reuse of existing designs, and makes it possible to address much larger systems. A central item of SACRES is the DC+ format for synchronous languages, which provides the common semantic framework for all tools as well as end user specification formalisms (StateMate and Sildex / Signal).
Keywords: embedded systems, safety critical systems, modular verification, distributed code generation, code validation and certification, synchronous languages, Statecharts, Signal.

A. Benveniste, T. Gautier, P. Le Guernic, E. Rutten.
Distributed code generation of dataflow synchronous programs: the SACRES approach.  Proceedings of The Eleventh International Symposium on Languages for Intensional Programming, ISLIP'98, Sun Microsystems, Palo Alto, California (USA), Mai 1998. (postscript)
Résumé : The SACRES project is an Esprit R&D project, Sacres members are: Siemens (Lead partner), i-Logix, TNI (Techniques Nouvelles d'Informatique), OFFIS, INRIA, the Weizmann Institute of Science, British Aerospace, SNECMA. SACRES is dealing with the development of new design methodologies and associated tools for safety critical embedded systems. Main targeted users are aeronautics, automobile, process control and energy. Emphasis has been put on formal techniques for modular verification of the specifications, distributed code generation, and generated code validation against specifications. These techniques aim at making more flexible the exploration of the software life cycle. Verification of the specifications and generated code validation aim at helping for certification of the overall design. Distributed code generation aims at reducing the dependency of the design with respect to the target architecture. In all cases, modularity helps reuse of existing designs, and makes it possible to address much larger systems. A central item of SACRES is the DC+ format for synchronous languages, which provides the common semantic framework for all tools as well as end user specification formalisms (StateMate and Sildex / Signal). In this paper, we mainly concentrate on the approach to distributed code generation.
Keywords: embedded systems, safety critical systems, distributed code generation, synchronous languages, Signal.

O. Kouchnarenko, S. Pinchinat.
Labeling Automata with Polynomials.  Proceedings of the International Workshop on Reasoning about Actions (joint to ESSLLI'98), Saarbrueken, Germany, Août 1998. (postscript)
Résumé : We present a behavioral model for discrete event systems based on a polynomial approach. We define implicit transition systems with associated combinators of parallel composition and event hiding, as well as an equivalence criterion called symbolic bisimulation. We also establish congruence properties of this equivalence. Further on, we explain the methodology applied to the synchronous language Signal, which domains of application range over the many fields of embedded systems, robotics, etc.
Keywords: Dynamic systems, event calculus, polynomials, behavioral equivalence, symbolic bisimulation, synchronous languages, model-checking.

O. Kouchnarenko, S. Pinchinat.
Intensional Approaches for Symbolic Methods.  Rapport de Recherche Irisa / Inria-Rennes, No3448, Juillet 1998. (postscript)
Résumé : We present a behavioral model for discrete event systems based on an intentional formalism, as a possible approach within the broader trend towards rich symbolic representations in verification. We define Intensional Labeled Transition Systems with associated combinators of parallel composition and event hiding, and we propose symbolic bisimulation to handle strong bisimulation intentionally. Further on, we explain how the methodology has been developed for the synchronous language Signal, via the verification tool Sigali.
Keywords: INTENSIONAL TRANSITION SYSTEMS / POLYNOMIALS,(SYMBOLIC) BISIMULATION / SYNCHRONOUS LANGUAGES / EQUIVALENCE CHECKING

O. Kouchnarenko, S. Pinchinat.
Intensional approachs for symbolic methods.  Electronic Notes in Theoretical Computer Science, 18, 1998. (postscript)
Résumé : We present a behavioral model for discrete event systems based on an intensional formalism, as a possible approach within the broader trend towards rich symbolic representations in verification. We define Intensional Labeled Transition Systems with associated combinators of parallel composition and event hiding, and we propose symbolic bisimulation to handle strong bisimulation intensionally. Further on, we explain how the methodology has been developed for the synchronous language Signal, via the verification tool Sigali.
Keywords: intensional transition systems, polynomials, (symbolic) bisimulation, synchronous languages, equivalence checking

A. Kountouris.
Outils pour la validation temporelle et l'optimisation de programmes synchrones.  Thèse de l'Université de Rennes 1, IFSIC, Octobre 1998. (postscript)
Résumé : Les travaux effectués dans le cadre de cette thèse visent à la définition éventuelle d'une méthodologie de conception-implémentation des systèmes réactifs temps-réel. Dans beaucoup de cas l'implémentation de tels systèmes est un problème de conception conjointe matériel-logiciel. Seule une architecture mixte, composée des processeurs standards et de circuits synthétisés (ASIC - Application Specific Integrated Circuits) est en effet susceptible de satisfaire les contraintes temps-réels imposées. Sur telles architectures certaines parties du traitement sont effectuées de manière performante améliorant ainsi la performance globale du système. Dans notre approche SIGNAL sert de formalisme de spécification et sa représentation interne comme représentation interne du système en cours de conception (design). L'activité centrale en co-design est l'exploration de l'espace de décision du concepteur (design space). Son efficacité dépend de l'existence des outils assistant le concepteur lors de la tâche d'évaluation/estimation des performances et des coûts. L'existence de tels outils rend possible l'expérimentation de plusieurs solutions avant de se décider sur une solution particulière et de procéder à son implémentation. Dans le cas des systèmes à caractère "temps critique" la performance a une plus grande priorité que le coût. Notre travail sur l'évaluation de performances, peut bénéficier de travaux déjà effectués par ailleurs dans le domaine de l'analyse à haut-niveau du temps d'exécution de programmes au pire cas (Worst Case Execution Time analysis). Dans la problématique d'analyse temporelle de haut-niveau, il est nécessaire de tenir compte des chemins d'exécution ainsi que des optimisations faites par les outils de compilation et finalement les caractéristiques des architectures cibles. En utilisant la représentation interne de SIGNAL et le calcul d'horloges nous montrons comment on peut améliorer l'analyse de chemins d'exécution, modéliser diverses optimisations et finalement produire des estimations sûres et de bonne qualité. Ensuite, la synthèse repose sur la capacité à se connecter aux outils existants via la génération automatique de code source accepté comme entrée par ces outils (i.e. compilateurs, outils de synthèse comportementale, optimiseurs etc.). La génération est automatique afin de garantir la correction du passage d'un langage à une autre. Actuellement les approches automatiques comparées aux approches manuelles sont moins performantes et pour cette raison le problème d'optimisation des résultats a été étudié. Une fois encore, la représentation interne de SIGNAL et le calcul d'horloges constituent un outil indispensable afin d'optimiser le processus de la génération automatique de code intermédiaire et ensuite d'aider les outils de synthèse à produire des résultats finaux de meilleure qualité. Enfin, ce qui est mis en évidence est la capacité de SIGNAL et de sa représentation interne à unifier le processus de développement, non seulement en permettant de spécifier sous le même formalisme des sous-systèmes aux implémentations différentes (en matériel ou en logiciel), et appartenant à des domaines d'application différents (traitement du signal ou contrôle), mais aussi en unifiant les diverses activités nécessaires à travers les différentes phases de développement sous la même représentation interne. Le Graphe Hiérarchisé aux Dépendances Conditionnées (GHDC) et le calcul d'horloges peuvent renforcer et, dans certains cas, améliorer les résultats des techniques existantes.
Keywords: Temps-réel, programmation synchrone, représentation interne, évaluation de performances, simulation, optimisation, génération de code, conception conjointe matériel-logiciel

P. Le Guernic, S. Machard, E. Rutten.
Répartition de programmes Signal.  Actes des Rencontres Francophones du Parallélisme des Architectures et des Systèmes, RenPar'10, Strasbourg, Juin 1998. (postscript)
Résumé : Signal, un langage synchrone et orienté flot de données, permet la spécification d'applications temps réel sûres. Le compilateur utilise un seul formalisme tout au long de la chaîne de conception, de la spécification à la preuve de propriétés, la génération de code et la validation. Dans ce papier, nous allons montrer comment il est possible de répartir un programme Signal en utilisant ce formalisme. La répartition proposée est donnée par l'utilisateur, elle consiste en un ensemble de transformations respectant la sémantique du langage et son ouverture vers des outils de preuve et de validation.
Keywords: Programmation synchrone, Signal, répartition fonctionnelle, génération de code distribué.

H. Marchand, M. Le Borgne.
Partial Order Control of Discrete Event Systems modeled as Polynomial Dynamical Systems.  1998 IEEE International Conference On Control Applications, Trieste, Italie, Septembre 1998. (postscript)
Résumé : In this paper, we address computational methods for the synthesis of controllers for discrete event systems modeled as polynomial dynamical systems over \zzz. The control objectives are specified as order relations to be checked by the system. The control objectives equations are then synthesized using algebraic tools. The applications of these methods to the safety specification of a power transformer station controller is presented.
Keywords: Control Synthesis, Polynomial Dynamical System, Order Relations, Power systems.

H. Marchand, M. Le Borgne.
On the Optimal Control of Polynomial Dynamical Systems over Z/pZ.  4th IEE International Workshop on Discrete Event Systems, pages 385-390, Cagliari, Italie, Août 1998. (postscript)
Résumé : This paper describes how a polynomial equationnal approach of the theory of logic discrete event systems leads to efficient algorithms for the synthesis of supervisory controllers. Even if traditional control objectives can be considered in our framework ({\it invariance

H. Marchand, O. Boivineau, S. Lafortune.
On the Synthesis of Optimal Schedulers in Discrete Event Control Problems with Multiple Goals.  1998 IEEE International Conf. On Systems, Man, And Cybernetics, pages 734-739, San Diego, California, USA, Octobre 1998. (postscript)
Résumé : This paper deals with a new type of optimal control for Discrete Event Systems that extends the theory of \cite{sengupta98

H. Marchand, P. Bournai, M. Le Borgne, P. Le Guernic.
A Design Environment for Discrete-Event Controllers based on the SIGNAL Language.  1998 IEEE International Conf. On Systems, Man, And Cybernetics, pages 770-775, San Diego, California, USA, Octobre 1998. (postscript)
Résumé : In this paper, we present the integration of a controller synthesis methodology in the Signal environment through the description of a tool dedicated to the algebraic computation of a controller and then to the simulation of the controlled system. The same language is used to specify the physical model of the system and the control objectives. The controller is then synthesized using the formal calculus tool Sigali. The result is then automatically integrated in a new Signal program in order to obtain a simulation of the result.
Keywords: Control theory, Polynomial dynamical system, Synchronous Methodology, Signal.

H. Marchand, O. Boivineau, S. Lafortune.
On the Synthesis of Optimal Schedulers in Discrete Event Control Problems with Multiple Goals.  Rapport de Recherche CGR-98-10, Control Group, College of Engineering, Univeristy of Michigan, USA, Juillet 1998. (postscript)
Résumé : This paper deals with a new type of optimal control for Discrete Event Systems. Our control problem extends the theory of \cite{sengupta98

D. Nowak, J.R. Beauvais, J.P. Talpin.
Co-Inductive Axiomatization of a Synchronous Language.  Theorem Proving in Higher Order Logics (TPHOLs'98), Springer, LNCS 1479, pages 387-399, Septembre 1998. (postscript)
Résumé : Over the last decade, the increasing demand for the validation of safety critical systems lead to the development of domain-specific programming languages (e.g. synchronous languages) and automatic verification tools (e.g. model checkers). Conventionally, the verification of a reactive system is implemented by specifying a discrete model of the system (i.e. a finite-state machine) and then checking this model against temporal properties (e.g. using an automata-based tool). We investigate the use of a theorem prover, COQ, for the specification of infinite state systems and for the verification of co-inductive properties.
Keywords: synchronous programming, co-induction, theorem proving

S. Pinchinat, E. Rutten, R.K. Shyamasundar.
Taxonomy and expressiveness of preemption : a syntactic approach.  Proceedings of the Asian Computing Science Conference, ASIAN'98, LNCS, Manila, The Philippines, Décembre 1998. (postscript)
Résumé : We propose a taxonomy of preemptive ( suspensive and abortive) operators capturing the intuition of such operators that exist in the various synchronous languages. Some of the main contributions of the paper are: a precise notion of preemption is established at a structural level ; we show that the class of suspensive operators is strictly more expressive than abortive operators, and we show that suspension is primitive while abortion is not. The proof techniques relies on a syntactic approach, based on SOS-specification formats, to categorize the different preemption features ; also an equivalence criterion between operators specifications is proposed to provide us with expressive power measurement.
Keywords:

I. Smarandache.
Transformations affines d'horloges: application au codesign de systèmes temps-réel en utilisant les langages Signal et Alpha.  Thèse de l'Université de Rennes 1, IFSIC, Octobre 1998. (postscript)
Résumé : Cette thèse s'inscrit dans le cadre du développement du langage SIGNAL dont les objectifs sont la spécification et la mise en oeuvre d'applications temps-reel critiques. Nos travaux ont concerné l'extension du compilateur de SIGNAL qui est un outil formel pour la vérification des contraintes de synchronisation d'horloges en SIGNAL. De manière plus générale, notre étude se situe dans un contexte de conception conjointe de systèmes mixtes matériel/logiciel (codesign) pour laquelle l'environnement de programmation de SIGNAL s'est prouvé très adapté. Dans ce contexte, nous avons constaté que les langages SIGNAL et ALPHA possèdent des propriétés complémentaires concernant la programmation de traitements numériques importants reliés par du contrôle. ALPHA est un langage fonctionnel pour la spécification et l'implémentation d'algorithmes réguliers, tandis que l'apport de SIGNAL se manifeste dans le domaine du contrôle. L'interfaçage des deux langages a relevé le problème du raffinement des spécifications mixtes et leur validation. Les transformations de spécifications ont induit des transformations affines sur les horloges SIGNAL et la nécessité de mettre en place un calcul formel sur les synchronisations des horloges transformées. Le nouveau calcul formel mis en place est basé sur un ensemble de règles de synchronisabilité déduites à partir des propriétés des transformations affines. Nous avons retrouvé des conditions de synchronisabilité basées sur un calcul d'entiers qui nous ont permis d'étendre les capacités de preuve formelle du compilateur de SIGNAL. Nous avons validé le calcul de synchronisabilité proposé et les concepts liés à la conception conjointe avec SIGNAL et ALPHA à travers une application du domaine de codage d'images vidéo.
Keywords: Temps-réel, programmation synchrone, conception conjointe matériel/logiciel, transformation affine, calcul d'horloges, synchronisabilité

J.P. Talpin, A. Benveniste, B. Caillaud, C. Jard, Z. Bouziane, H. Canon.
BDL, a language of distributed reactive objects.  Rapport de Recherche Irisa / Inria-Rennes, No3353, Février 1998. (postscript)
Résumé : We introduce the definition of a language of distributed reactive objects, BDL, as a unified medium for specifying, verifying, compiling and validating object-oriented, distributed reactive systems. One of the novelties in BDL is its seamless integration into UML. BDL supports a description of objects interaction which respects both the functional architecture of system designs and the declarative style of diagram descriptions. This support is implemented by means of a pre-order theoretical framework which allows to specify both the causality and the control models of object interactions independently of any hypothesis on the actual configuration of the system. Given the description of such a configuration, BDL\ offers new perspectives for a flexible verification of systems by modeling them as an asynchronous network of synchronous components. It allows an optimized code generation by using compilation techniques developed for synchronous languages. It permits an accurate validation and test of applications by supporting the manipulation of both causal and control dependencies. BDL aims at maximizing the re-usability of high-level specifications while minimizing programming effort and test-case based validation of distributed systems.
Keywords: Programming languages, reactive and distributed systems, object-oriented methodology

Webmaster : epatr_webmaster@irisa.fr Ces pages sont créées automatiquement par le programme bib2html du projet Vista de l'IRISA-INRIA Rennes