Publications 1996
D. Chauveau.
Étude d'une extension du langage synchrone SIGNAL aux modèles probabilistes : le langage SIGNalea. Thèse de l'Université de Rennes 1, Décembre 1996. (postscript)
Résumé : L'absence d'outils ergonomiques pour le traitement de systèmes stochastiques complexes, comme on peut en trouver dans de nombreuses applications industrielles, a conduit le projet EP-ATR de l'Irisa à envisager la réalisation d'une extension du langage de programmation SIGNAL pour la manipulation de systèmes hybrides stochastiques/non-stochastiques. Développé depuis une dizaine d'années, le langage SIGNAL est un langage flot de données de type équationnel, appartenant à la famille des langages synchrones et destiné à la spécification de systèmes réactifs temps-réel. Une interface graphique intégrée à l'environnement SIGNAL permet de spécifier des programmes de façon modulaire et hiérarchique sous la forme de boîtes interconnectées. La définition de SIGNalea a dès le début soulevé des problèmes mathématiques complexes, dont une étude approfondie a conduit à la définition du formalisme mathématique CSS. Le modèle CSS ne s'intéresse qu'aux cas où le système étudié met en jeu un nombre fini de variables. Les objets de base de ce modèle sont des systèmes hybrides stochastiques/non-stochastiques. Nous définissons sur ces systèmes une généralisation de la règle de Bayes qui nous permet d'obtenir des méthodes de simulation et d'estimation incrémentales se rapprochant assez fortement des travaux de A.-P. Dempster et G. Shafer en Statistique et Intelligence Artificielle sur les fonctions de croyance et réseaux de croyance. La version de SIGNalea que nous présentons est sur une généralisation du langage SIGNAL qui permet d'inclure des ``bulles'' de type CSS. Elle donne la possibilité de spécifier tout système dynamique aléatoire de type ``automate stochastique'', ou ``Hidden Markov Model'' (HMM). Dans le cas booléen, le calcul des primitives intervenant pour la simulation Bayesienne a été implémenté en utilisant des techniques BDD (Binary Decision Diagrams). Enfin, nous apportons un élément nouveau au modèle CSS qui est la prise en compte de la hiérarchie des systèmes dans les algorithmes de simulation et d'estimation incrémentales.
Keywords:
A. Kountouris, C. Wolinski.
A real-time hw/sw co-design approach based on the language and its environment. Rapport de Recherche Irisa, No1053, Octobre 1996. (postscript)
Résumé : In the present document the idea of building around the SIGNAL language and its environment, a methodology for the evaluation of implementation alternatives, design space exploration and implementation of R/T systems, is investigated. The driving force behind this effort is the desire to exploit the advantage SIGNAL in the domain of functional specification, as well as the numerous tools built around it. A Real-Time co-design methodology is proposed and the basic tools that will assist the user in the development process, are described. Such a methodology intends to bridge the existing gap in the SIGNAL environment between specification and actual implementation.
Keywords: specification, SIGNAL, methodology, Real-Time, hw/sw co-design
M. Le Borgne, H. Marchand, E. Rutten, M. Samaan.
Formal Verification of SIGNAL programs: Application to a Power Transformer Station Controller. Proceedings of the Fifth International Conference on Algebraic Methodology and Software Technology AMAST'96, Springer-Verlag, LNCS 1101, pages 271-285, Munich, Germany, Juillet 1996. (postscript)
Résumé : We present a methodology for the verification of reactive systems, and its application to a case study. Systems are specified using the synchronous data flow language Signal. As this language is based on an equational approach (ie Signal programs are constraint equations between signals), it is natural to translate its boolean part into a system of polynomial equations over three values denoting true, false and absent (ie over Z/3Z). Using operations in algebraic geometry of polynomials, it is possible to check properties concerning the system, such as liveness, invariance, reachability and attractivity. We apply this method to the verification of the automatic circuit-breaking control system of an electric power transformer station. This system handles the reaction to electrical defects on high voltage lines.
Keywords: Reactive systems, synchronous language, verification, case study.
P. Le Guernic, E. Rutten.
Experiments with the synchronous methodology illustrating its support of predictability. Proceedings of the 21st IFAC/IFIP Workshop on Real Time Programming, WRTP'96, pages 81-86, Canela/Gramado, RS, Brazil, Novembre 1996. (postscript)
Résumé : This paper analyses experiments with the Signal programming environment for the design of safety-critical systems, with an emphasis on predictable behaviour. This environment is based upon a data-flow language and a synchronous model; the composition of interacting sub-systems and tasking of data-flow processes do not introduce unpredictability. It offers integrated tools for transformations and analysis. The practical relevance of the synchronous model and methodology is illustrated with a focus on predictabilty by examples gathered from a spectrum of experiments (robot vision, production cell control and power transformer control).
Keywords: Reactive systems, synchronous language, predictability, experiments.
H. Marchand, E. Marchand, E. Rutten.
Spécification et vérification de systèmes réactifs : expérimentation de la méthodologie synchrone SIGNAL. Actes du Congrès AFCET sur la Modélisation des Systèmes Réactifs, MSR'96, Brest, Mars 1996. (postscript)
Résumé : Signal est un langage synchrone flot de données, étendu par des tâches préemptives dans Signalgti. Il est ainsi adapté à la spécification de systèmes réactifs présentant une dualité continu (échantillonné) et discret (événementiel ou séquentiel). La vérification formelle de leur correction se fait dans un modèle équationnel. Deux exemples de systèmes réactifs serviront de support à cet article.
Keywords: Systèmes réactifs, langage synchrone, flot de données, préemption de tâches, verification formelle.
C. Paller, C. Wolinski.
Springplay : répartition et ordonnancement de tâches pour leur exécution en « pipeline ». Rapport de Recherche Irisa, No1052, Octobre 1996. (postscript)
Résumé : Cet article présente un algorithme nommé "Springplay" destiné à la répartition et l'ordonnancement statique de tâches pour leur exécution en "pipeline" dans des systèmes hétéro gènes. L'algorithme présenté emploie une approche globale pour l'optimisation du temps d'exécu tion. La même approche a été utilisée dans la version précédente de cet algorithme destinée à l'exécution non "pipelinée" de tâches. Dans cet algorithme on utilise des "distances" pour mesurer le degré d'appartenance d'un noeud au processeur et des "forces" pour modifier sa position. L'algo rithme présenté se réfère à certaines classes de réseaux de neurones.
Keywords: ordonnancement statique, exécution parallèle, architecture hétérogène, conception conjointe
Les documents contenus dans ces répertoires sont rendus disponibles par les
auteurs qui y ont contribué en vue d'assurer la diffusion à temps de travaux
savants et techniques sur une base non-commerciale. Les droits de copie et
autres droits sont gardés par les auteurs et par les détenteurs du copyright,
en dépit du fait qu'ils présentent ici leurs travaux sous forme électronique.
Les personnes copiant ces informations doivent adhérer aux termes et
contraintes couverts par le copyright de chaque auteur. Ces travaux ne peuvent
pas être rendus disponibles ailleurs sans la permission explicite du détenteur
du copyright.
