Publications 1999

J.R. Beauvais.
Modélisation de StateCharts en Signal pour la conception de systèmes critiques temps-réel.  Thèse de l'Université de Rennes 1, IFSIC, Janvier 1999. (postscript)
Résumé : Certains systèmes se révèlent posséder à la fois des aspects discrets et continus et un choix parmi les deux approches est souvent difficile. Nous proposons d'utiliser STATECHARTS pour les spécifications dirigées par les événements et les aspects séquentiels, et SIGNAL pour la spécification des systèmes continus. La consistance globale de la spécification est garantie car la traduction de STATECHARTS en SIGNAL donne une sémantique non ambigüe des STATECHARTS. On se propose ensuite d'utiliser SIGNAL comme représentation interne et pour les divers traitements symboliques à appliquer au système. Cette thèse décrit une méthode de traduction depuis STATEMATE vers le langage équationnel SIGNAL. Cette traduction vers SIGNAL en tant que représentant de la classe des langages synchrones déclaratifs : - offre un moyen de mélanger des langages synchrones impératifs et déclaratifs simplement en composant des équations (composition de processus SIGNAL), - donne une sémantique totalement synchrone des STATECHARTS basée sur la sémantique de SIGNAL, - ouvre une connexion directe depuis STATECHARTS vers la boîte à outils SIGNAL : compilateur, simulateur, outils de vérification, - permet l'extraction d'une hiérarchie d'horloges à partir d'une spécification STATECHARTS, - permet au compilateur, par l'utilisation de cette hiérarchie d'horloges, de produire un code efficace / distribué / compact depuis un STATECHARTS.
Abstract : Some systems happen to have discrete and continuous aspects and a choice between the two approaches is often difficult. We suggest to use STATECHARTS for the event-driven specifications and for the sequential aspects, and SIGNAL for the specification of the continuous systems. The global consistency of the specification is guaranty because the translation of STATECHARTS into SIGNAL gives a non-ambiguous semantics of STATECHARTS. We propose then to use SIGNAL as an internal representation for different symbolic treatment to apply to the system. This thesis describe a translation method from STATEMATE into the equational language SIGNAL. SIGNAL being a representative of the class of declarative synchronous languages, this translation: - provides a way to merge imperative and declarative synchronous languages by simply composing equations (composition of SIGNAL processes), - gives a compositional definition of the considered STATECHARTS semantics, - opens a direct connection from a STATECHARTS design to the SIGNAL tools: compiler, simulator, verification system, - one of these tools is a code generator that can produce / efficient / distributed / compact code from a STATECHARTS specification using the clock calculus available in SIGNAL.

A. Benveniste, P. Caspi.
Distributing synchronous programs on a loosely synchronous, distributed architecture.  Rapport de Recherche Irisa, No1289, Décembre 1999. (postscript)
Résumé : In this short note we discuss the distribution of synchronous programs on distributed, asynchronous architecture of the type preferred for embedded real-time control applications. In such architectures, no global clock is broadcast. Instead, the bus, as well as its users are triggered by local periodic clocks. To improve fault-tolerance and robustness, these clocks are not synchronized, neither physically nor logically. Therefore such an architecture has some (restricted) degree of asynchrony, we call it loosely synchronous. A typical example of such architecture is the osek protocol, used for embedded electronics in automotive industry. In this note we show how synchronous programs can be safely distributed on loosely synchronous architectures. The method described here may not be novel to some communities, but it aims at ensuring awareness of the community of engineers in the area of real-time, embedded control systems.
Keywords: Synchronous languages, desynchronization, distributed code generation, loosely synchronous.

A. Benveniste, B. Caillaud, P. Le Guernic.
From synchrony to asynchrony.  Rapport de Recherche Irisa, No1233, Mars 1999. (postscript)
Résumé : We present an in-depth discussion of the relationships between synchrony and asynchrony. Simple models of both paradigms are presented, and we state theorems which guarantee correct desynchronization, meaning that the original synchronous semantics can be reconstructed from the result of this desynchronization. Theorems are given for both the desynchronization of single synchronous programs, and for networks of synchronous programs to be implemented using asynchronous communication. Assumptions for these theorems correspond to proof obligations that can be checked on the original synchronous designs. If the corresponding conditions are not satisfied, suitable synchronous mini-programs which will ensure correct desynchronization can be composed with the original ones. This can be seen as a systematic way to generate ``correct protocols'' for the asychronous distribution of synchronous designs. The whole approach has been implemented, in the framework of the SACRES project, within the SILDEX tool marketed by TNI, as well as in the SIGNAL compiler.
Keywords: Synchronous languages, desynchronization

L. Besnard, P. Bournai, T. Gautier, N. Halbwachs, S. Nadjm-Tehrani, A. Ressouche.
Design of a multi-formalism application and distribution in a data-flow context: an example.  Proceedings of The 12th International Symposium on Languages for Intensional Programming, ISLIP' 99, NCSR Demokritos, Athens, Greece, Juin 1999. (postscript)
Résumé : This paper describes a multi-formalism experiment design in the domain of real-time control systems. It uses several synchronous languages on a case study which is a realistic industrial example. Co-simulation is provided through the use of a common format, and automatic distributed code generation is experimented in the context of the graphical environment of the data-flow language SIGNAL.

T. Gautier, P. Le Guernic.
Code generation in the SACRES project.  Towards System Safety, Proceedings of the Safety-critical Systems Symposium, SSS'99, Springer, Huntingdon, UK, Février 1999. (postscript)
Résumé : The SACRES project is dealing with the development of new design methodologies and associated tools for safety critical embedded systems. Emphasis is put on formal techniques for modular verification of the specifications, distributed code generation, and generated code validation against specifications. This is allowed by using a single formal model which is that of the DC+ format, which provides a common semantic framework for all tools as well as end user specification formalisms. Modular and distributed code generation is the main subject of this paper. Distributed code generation aims at reducing the dependency of the design with respect to the target architecture. Modularity helps reuse of existing designs, and makes it possible to address much larger systems.
Keywords:

F. Jiménez, E. Rutten.
A synchronous model of the PLC programming language ST.  Proceedings of the Work In Progress session, 11th Euromicro Conference on Real Time Systems, ERTS'99, pages 21--24, York, England, Juin 1999. (postscript)
Résumé : This paper presents first results in the definition of a synchronous model of the PLC programming language ST. This work is part of the integration of the IEC 1131 design standard and the synchronous technology, with the motivation to give access to formal techniques and tools.

F. Jiménez, E. Rutten.
Modélisation synchrone de standards de programmation de systèmes de contrôle.  Actes de la Journée d'études sur les Nouvelles Percées dans les Langages pour l'Automatique, Amiens, Novembre 1999. (postscript)
Résumé : Dans le domaine des automatismes industriels, les contrôleurs ont souvent une grande criticité quant à la sûreté de leur opération, et une grande complexité. Leur conception sûre et leur analyse requièrent donc le support d'outils automatisés. L'approche synchrone propose justement des méthodes formelles pour lesquelles il existe une technologie effective et industrielle, offrant un support pour la vérification, la simulation, l'évaluation des performances, la compilation et génération de code. Notre approche consiste à étudier la norme CEI 1131-3 en vue de son intégration avec la technologie synchrone dans un environnement de conception. On présente en particulier des résultats de modélisation du langage ST en Signal.

M. Kerboeuf, D. Nowak, J.-P. Talpin.
The steam-boiler problem in SIGNAL-COQ.  Rapport de Recherche Irisa / Inria-Rennes, No3773, Octobre 1999. (postscript)
Résumé : Among the various formalisms for the design of reactive systems, the SIGNAL-COQ formal approach, i.e. the combined use of the synchronous dataflow language SIGNAL and the proof assistant COQ, seems to be especially suited and practical. Indeed, the deterministic concurrency implied by the synchronous model on which SIGNAL is founded strongly simplifies the specification and the verification of such systems. Moreover, COQ is not limited to some kind of properties and so, its use enables to disregard what can be checked during the specification stage. In this article, we underline the various features of this SIGNAL-COQ formal approach with a large scale case study, namely the Steam Boiler problem.
Keywords: Reactive Systems / Synchronous Model / Verification / Model Checking / Proof Assistant / Co-Induction

H. Marchand, M. Samaan.
On the Incremental Design of a Power Transformer Station Controller using Controller Synthesis Methodology.  World Congress on Formal Methods (FM'99), Volume 1709 of LNCS, pages 1605-1624, Toulouse, France, Octobre 1999. (postscript)
Résumé : In this paper, we describe the incremental specification of a power transformer station controller using a controller synthesis methodology. We specify the main requirements as simple properties, named control objectives, that the controlled plant has to satisfy. Then, using algebraic techniques, the controller is automatically derived from these set of control objectives. In our case, the plant is specified at a high level, using the data-flow synchronous Signal language and then by its logical abstraction, named polynomial dynamical system. The control objectives are specified as invariance, reachability, attractivity properties, as well as partial order relations to be checked by the plant. The control objectives equations are then synthesized using algebraic transformations.
Keywords: Discrete Event Systems, Polynomial Dynamical System, Supervisory Control Problem, \signal, Power Plant.

H. Marchand, M. Le Borgne.
The Supervisory Control Problem of Discrete Event Systems using polynomial Methods.  Rapport de Recherche Irisa, No1271, Octobre 1999. (postscript)
Résumé : This paper regroups various studies achieved around polynomial dynamical system theory. It presents the basic algebraic tools for the study of this particular class of discrete event systems. The polynomial dynamical systems are defined by polynomial equations over \zzz. Their study relies on concept borrowed from elementary algebraic geometry: varieties, ideals and morphisms. They are the basic tools that allow us to translate properties or specifications from a geometric description to suitable polynomial computations. In this paper, we more precisely describe the controller synthesis methodology. We specify the main requirements as simple properties, named control objectives, that the controlled plant has to satisfy.The plant is specified as a polynomial dynamical system over \zzz. The control of the plant is performed by restricting the controllable input values to values suitable with respect to the control objectives. This restriction is obtained by incorporating new algebraic equations into the initial polynomial dynamical system, which specifies the plant. Various kind of control objectives are considered, such as ensuring the {\it invariance

D. Nowak, J.P. Talpin, P. Le Guernic.
Synchronous Structures.  Proceedings of the 10th International Conference on Concurrency Theory (CONCUR'99), Volume 1664 of LNCS, Springer Verlag, Août 1999. (postscript)
Résumé : Synchronous languages have been designed to ease the development of reactive systems, by providing a methodological framework for assisting system designers from the early stages of requirement specifications to the final stages of code generation or circuit production. Synchronous languages enable a very high-level specification and an extremely modular design of complex reactive systems by structural decomposition them into elementary processes. We define an order-theoretical model that gives a unified mathematical formalization of all the above aspects of the synchronous methodology (from relations to circuits). The model has been specified and validated using a theorem prover as part of the certified, reference compiler of a synchronous programming language.
Keywords: reactive systems, synchronous programming, order theory, category theory.

D. Nowak.
Spécification et preuve de systèmes réactifs.  Thèse de l'Université de Rennes 1, IFSIC, Octobre 1999. (postscript)
Résumé : Ces dernières années, la vérification des systèmes informatiques critiques est devenue un sujet de recherche important en raison du développement croissant de logiciels pour la médecine, les moyens de transports ou les centrales nucléaires. Dans ces domaines, une erreur de programmation peut coûter très cher financièrement ou en vies humaines. Dans ce cadre, les informaticiens ont été amenés à développer des langages dits synchrones dédiés à la programmation des systèmes réactifs. Un système réactif est un système qui réagit continûment avec son environnement à une vitesse imposée par son environnement. Il ne termine pas forcément et peut être concurrent. En général, la concurrence entraîne le non-déterminisme mais le modèle synchrone se distingue par le fait qu'il fait cohabiter concurrence et déterminisme. Dans cette thèse, nous formalisons dans l'outil d'aide à la preuve Coq une version co-inductive de la sémantique des traces du langage synchrone Signal. Nous utilisons la co-induction car nous pensons qu'il s'agit là d'un outil mathématique naturel et simple pour manipuler des objets infinis tels que les signaux. La pratique nous permet de confirmer que la co-induction est un outil efficace pour prouver la correction d'un système réactif spécifié en Signal. Afin de pouvoir traiter la causalité dans les programmes synchrones, nous généralisons ensuite cette approche en développant une variante des structures d'événements que nous appelons les structures synchrones. Par cette approche, il est possible de traiter les dépendances conditionnées entres signaux et il n'est pas nécessaire de dénoter l'absence d'un signal par une valeur spéciale comme cela est fait usuellement. C'est plus en accord avec la réalité car l'absence d'un signal doit être inférée par le programme (endochronie).
Mots clefs : Programmation synchrone, outil d'aide à la preuve, structure synchrone.
Abstract : In recent years, the verification of safety critical systems has become an area of increasing importance in computer science because of the constant progression of software developments in sensitive fields like medicine, communication, transportation and (nuclear) energy. Such systems are often concurrent. These strong requirements have led to the development of specific programming languages and related verification tools for concurrent systems. We focus our research on concurrent systems that continuously react to their environment at a speed determined by this environment. They are called reactive systems Synchronous languages, such as Signal, are best suited for the design of reactive systems. Synchronous languages enable a very high-level specification and an extremely modular implementation of complex systems by structurally decomposing them into elementary synchronous processes. We investigate the use of a proof assistant for the specification of infinite state systems and for the verification of co-inductive properties. We formalize the trace semantics of Signal within the proof assistant Coq. We choose to use co-inductive features of Coq because we find it is a natural and simple mathematical tool to handle infinite objects such as signals. Our practice confirms that this is also an efficient way to prove correctness properties of reactive systems specified in Signal. We then generalize our previous approach to be able to deal with causality in synchronous programs. We develop a variant of event structures that we call synchronous structures. Within this approach, we can deal with causality and we need not denote the absence of a signal by a special value as it is done usually. It is more consistent with reality because the absence of a signal has to be inferred by the program (endochrony).
Keywords: Synchronous programming, proof assistant, synchronous structure.

S. Pinchinat, H. Marchand, M. LeBorgne.
Symbolic Abstractions of Automata and their application to the Supervisory Control Problem.  Rapport de Recherche Irisa, No1279, Novembre 1999. (postscript)
Résumé : In this report, we describe the design of abstraction methods based on symbolic techniques: classical abstraction by state fusion has been considered. we present a general method to abstract automata on the basis of a state fusion criterion, derived from e.g. equivalence relations (such as bisimulation), partitions, ... We also introduced other kinds of abstraction, falling into the category of abstraction by restriction: in particular, we studied the use of the controller synthesis methodology to achieve the restriction synthesis. The methods rely on symbolic representation of the labeled transition system, namely the Intensional Labeled Transition System (ILTS). It is a behavioral model for Discrete event systems based on polynomial approach, that has effective applications for the analysis of Signal programs. We finally apply this methodology to solve the Supervisory Control Problem.
Keywords: Intentional transition systems, polynomials, symbolic bisimulations, model reduction, BDD, Supervisory control Problem

I. Smarandache, T. Gautier, P. Le Guernic.
Validation of Mixed Signal-Alpha Real-Time Systems through Affine Calculus on Clock Synchronisation Constraints.  World Congress on Formal Methods (FM'99), Volume 1709 of LNCS, pages 1364-1383, Toulouse, France, Octobre 1999. (postscript)
Résumé : 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. 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.

J.-P. Talpin, A. Benveniste, P. LeGuernic.
Asynchronous deployment of synchronous transition systems.  Rapport de Recherche Irisa, No1269, Octobre 1999. (postscript)
Résumé : The synchronous model of concurrency has demonstrated its practicality for the design of circuits, embedded systems, reactive systems. This model allows to base design on deterministic concurrency, which is much easier to deal with than classical, nondeterministic, asynchronous concurrency. Compiling, optimizing, and verifying programs is done using powerful techniques. On the other hand, UML is now establishing as a standard framework for object oriented software design and methodologies. UML provides a coherent set of views of the system under design. Using UML for reactive systems design raises some difficulties, however, of which a major is usually the complexity of system behaviour. While UML offers notations to handle behaviours, there is little agreement on a formal semantics for such notations. While it is often argued that a loose semantics may be an advantage at the requirements capture, it may be of interest to build upon strong semantic foundations when formal manipulations are considered, including verification, optimization and rewriting, code and architecture generation. Our aim is to take advantage of the rich background of synchronous programming technology for this purpose, and present a formalism called BDL, based on the mathematical notion of pre-orders, to address the key issues raised by the avant of de-facto methodological standards in the context of distributed, reactive, systems design, that none of the existing formalisms yet comply with. Namely: architecture deployment, partial designs, inheritance and reuse, compliance to UML and dynamicity.
Keywords: Synchronous programming, transition systems, desynchronization, compilation

J.-P. Talpin, A. Benveniste, B. Caillaud, P. LeGuernic.
Hierarchic Normal Forms for desynchronization.  Rapport de Recherche Irisa, No1288, Décembre 1999. (postscript)
Résumé : Based on an earlier work, we present an in-depth discussion of the relationships between synchrony and asynchrony. Simple models of both paradigms are presented, and we state theorems which guarantee correct desynchronization, meaning that the original synchronous semantics can be reconstructed from the result of this desynchronization. This theory can be used as a basis for correct distributed code generation. The present paper presents a new data structure, the hierarchic normal form for a transition relation, which is instrumental in implementing this theory. We illustrate this on a Statecharts example. The whole approach is implemented in the SIGNAL compiler.
Keywords: Synchronous languages, desynchronization, distributed code generation

S. Tudoret.
Signal-Simulink : Hybrid System Co-simulation.  Rapport de Recherche Linköping, No20, Décembre 1999. (postscript)
Résumé :
This report presents an approach to simulating hybrid systems. We show how a discrete controller that controls a continuous environment can be co-simulated with the environment (plant) using C-code generated automatically from mathematical models. This approach uses SIGNAL with SIMULINK to model complex hybrid systems. The choices are motivated by the fact that SIGNAL is a powerful tool for modelling complex discrete behaviours and SIMULINK is well-suited to deal with continuous dynamics. We present various alternatives for implementing the communication between the plant and the controller, and how the MATLAB code generation mechanism in Real-time Workshop can be used for this purpose. Finally, we present interesting scenarios in the co-simulation of a discrete controller with its environment: a non-trivial siphon pump proposed by the Swedish engineer Christofer Polhem in 1697.

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