Publications 1995
P. Amagbegnon, P. Le Guernic, H. Marchand, E. Rutten.
The Signal data flow methodology applied to a production cell. Rapport de Recherche Irisa, No917, Mars 1995. (postscript)
Résumé : This report presents a method to specify, verify and implement a controller for a robotic production cell using the Signal approach. This work has been performed as part of a case study concerning a production cell, proposed by FZI of Karlsruhe. Our contribution to this case study aims at illustrating the methodology associated with the Signal synchronous data flow language for the specification and implementation of control systems, as well as the verification of statical and dynamical properties using a proof system for Signal programs. We describe the full development of the example, specifying a generic controller, safe for all scheduling scenarios. The specification is structured in a modular way, using two decomposition principles: one following the architecture of the production cell, the other one separating the controller from the model of the system to be controlled. The latter point lies the originality of the approach, compared to imperative methods: the declarative language is used to specify, in the form of equations on signals, the behaviour of a system, and a controller putting constraints on it This way, one can build hierarchies of nested controlled systems: in the case of the production cell, the scheduled behaviour is a controlled instance of the safe behaviour, which is itself a controlled instance of the natural behaviour. The model of the production cell is made in terms of events and boolean data, abstracting from the numerical nature of part of the sensor data; this enables the formal analysis of the logical properties of the system. The equational nature of the Signal language leads naturally to the use of methods based on systems of polynomial dynamic equations over Z/3Z for the formal proof of the satisfaction of application's requirements.
Keywords: Specification, verification, real-time systems, synchronous language, data flow, robotic production cell.
T. Amagbegnon.
Forme canonique arborescente deshorloges de Signal. Thèse de l'université de Rennes 1, Novembre 1995. (postscript)
Résumé : Cette thèse traite des techniques de calcul booléen mises en oeuvre dans la compilation du langage SIGNALC'est un langage synchrone destiné à la programmation de systèmes réactifs. La compilation d'un programme SIGNAL repose sur la résolution d'un système d'équations booléennes qui représente son contrôle. La résolution mise en oeuvre dans le compilateur tire parti de la spécificité des équations issues des programmes SIGNAL et un système d'équations résolu est représenté par un arbre dont chaque noeud est un BDD\ (Diagramme Binaire de Décision). Nous décrivons en détail la forme des systèmes d'équations booléennes de SIGNAL et motivons le choix d'une représentation arborescente. Nous montrons à l'aide d'une factorisation à supports disjoints que cette représentation arborescente est une forme canonique des systèmes d'équations résolus de SIGNAL. Ensuite, nous développons sur cette structure de données des algorithmes de minimisation logique pour générer du code efficace. Enfin, nous développons des algorithmes de projection de systèmes d'équations en vue d'une évolution vers de la compilation séparée et de la preuve de propriétés de sûreté. Tous ces nouveaux algorithmes ont été mis en oeuvre et comparés avec les algorithmes préexistants.
Keywords:
D. Chauveau, M. Bons.
Simulation d'un circuit électro-domestique en Signal. Rapport de Recherche Irisa, No971, Novembre 1995. (postscript)
Résumé : Nous décrivons dans ce document un simulateur de circuit électro-domestique. Une méthode de conception modulaire qui s'appuie sur les principes du langage Signal, approche synchrone du temps et programmation par équations, est présentée.
Keywords:
S. Donikian, E. Rutten.
Reactivity, concurrency, data flow and hierarchical preemption for behavioral animationn. Proceedings of the 5th Eurographics Workshop on Programming Paradigms in Graphics. R.C. Veltkamp, E.H. Blake (eds.), Programming Paradigms in Graphics, Springer, Computer Science, 169 Maastricht, the Netherlands, Septembre 1995. (postscript)
Résumé : Behavioural models offer the ability to simulate autonomous entities like organisms and living beings. Such entities are able to perceive their environment, to communicate with other creatures and to execute some decided actions either on themselves or on their environment. Building such systems requires the design of a reactive system treating flows of data to and from its environment, in a complex way needing modularity, concurrency and hierarchy, and involving task control and preemption. Accordingly, in this paper we address the adequateness to the decisional part of the behavioural model of the following programming paradigms: reactivity, concurrency, data-flow and hierarchical preemption. The reactive languages provide users with complete design environments for such systems. The specification of concurrent behaviours is naturally supported in the synchronous languages, and they address control-intensive applications (sequencing and preempting tasks) as well as computation-intensive applications (data-flow). Signalgti is an extension of the language Signal where data-flow processes can be composed into nested preemptive tasks. An application in the simulation of a transportation system shows how these programming paradigms can be of use, and how Signalgti can support their implementation.
J.V. Echagüe, Z. Habbas, S. Pinchinat.
Structural Operational Semantics for True Concurrency. Proc. of the 15th International Conference of the Chilean Computer Science Society, SCCC'95, Arica, Chili, Novembre 1995. (postscript)
Résumé : We show how to use a wide class of Structural Operational Semantics specifications for Truly Concurrent Semantics, whereas the classical approach is rather based on interleaving models. The models we consider are Asynchronous Transition Systems and their behaviors are defined by means of a classical truly concurrent bisimulation : ST-bisimulation. However, the definition of ST-bisimulation over Asynchronous Transition Systems is new and makes this equivalence better understood. Moreover, we explain how our result holds of many other truly concurrent bisimulations of the literature.
Keywords:
H. Marchand, E. Rutten, M. Samaan.
Synchronous design of a transformer station controller in Signal. Proceedings of the 4th IEEE Conference on Control Applications, CCA '95, Albany, New York, pages 754-759, Septembre 1995. (postscript)
Résumé : This paper presents the specification and validation verification of the automatic circuit-breaking control system of an electric power transformer station. It handles the reaction to electrical defects on the high voltage lines. The purpose of this study is to construct a discrete event control system based on digital technology. To this end, we use the synchronous approach to reactive real-time systems, and in particular the data flow language Signal, and its tools for specification, formal verification, simulation, and implementation. The hierarchical, state-based and preemptive controller is implemented with Signal and its extension for preemptive tasks Signalgti. A graphical simulator supports validation of the specification.
Keywords: power systems, discrete event systems, reactive systems, synchronous language
H. Marchand, E. Rutten, M. Samaan.
Specifying and verifying a transformer station in Signal and Signalgti. Rapport de Recherche Irisa, No916, Mars 1995. (postscript)
Résumé : We present the specification and verification of the automatic circuit-breaking behavior of an electric power transformer station using the synchronous approach to reactive real-time systems, and particularly the Signal language. The synchronous languages have a mathematical model supporting the various phases of the development of a control system: specification, verification, simulation, code generation, and implementation. Their semantics are at the base of the various tools dedicated to each phase and integrated into homogeneous design environments. The methodology associated with the data flow language Signal is demonstrated on the example of the functional description of a medium tension power transformer station and the specification of its automatic behavior upon the occurrence of an electrical default. The specification of the complex hierarchical, state-based and preemptive behavior is made in Signalgti, an extension of Signal with the notions of time intervals and preemptive tasks. For the validation of the specification, a graphical simulator is generated using the execution environment for Signal. Properties required by the application are proved to hold on the specification of the controller, using the proof method associated with Signal.
Keywords: Power systems, control systems, formal methods, real-time, synchronous language, data flow, task preemption, formal methods, verification tools, software safety.
S. Pinchinat, E. Rutten, R.K. Shyamasundar.
Preemption primitives in reactive languages (a preliminary report). Proceedings of the Asian Computing Science Conference, ACSC '95, Pathumthani, Thailand, LNCS, Springer-Verlag, Décembre 1995. (postscript)
Résumé : In this paper, we study preemption primitives in reactive languages such as Esterel and Signal (and its extension SignalGti) in a common framework. This enables us to compare behavioural/structural expressive powers of different languages and gives an insight into the complementarity of different control and data-flow abstractions in the reactive languages. Such a study also provides a basis on which a basic set of preemption primitives can be incorporated in reactive languages from the point of view of expressive completeness.
Keywords:
E. Rutten, F. Martinez.
Signalgti: implementing task preemption and time intervals in the synchronous data flow language Signal. Proceedings of the 7th Euromicro Workshop on Real-Time Systems, Odense, Denmark, IEEE Publ., Juin 1995. (postscript)
Résumé : This paper presents SignalGTi, the encoding and implementation of an extension to the reactive data flow language Signal with constructs for hierarchical task preemption. Tasks are defined as the association of a data-flow process with a time interval on which it is executed. The motivation for introducing these preemption structures is the need for the specification of different modes of interactions with the environment, and transitions between them (i.e. sequencing) in a nested way, especially in complex applications like robotics and discrete event control systems. A pre-processor to the Signal compiler implements the encoding of the new constructs in the data-flow framework. This way, both data-flow and tasking paradigms are available within the same language-level framework, and the tools of the Signal environment for optimization, simulation or proof are available.
Keywords:
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.
