Publications 2000

B. Caillaud, J.P. Talpin, J.M. Jezequel, A. Benveniste, C. Jard.
BDL: a semantics backbone for UML dynamic diagrams.  Rapport de Recherche Inria, No4003, Septembre 2000. (postscript)
Résumé : The UML (Unified Modelling Language) comprises various types of notations, to model the functional architecture, the behaviour of its components, and its deployment. Dynamic diagrams provide descriptions of the components and system behaviour. Examples of dynamic diagrams are collaboration and sequence diagrams to specify high level abstractions for sequences of actions involving several components of the system. Activity diagrams, state diagrams, and statecharts are used to specify the detailed behaviour of a single component. In this report we propose a new formalism, called BDL, to serve as a semantic backbone for dynamic diagrams of UML. BDL diagrams allow to provide a set of UML diagrams a global dynamic semantics. It allows to specify the behaviour of systems. It provides a common semantics to the different dynamic diagrams --- this report analyses in detail sequence diagrams and statecharts. Composing components requires different types of communication, synchronous or asynchronous. While a precise description of these choices is essential at deployment stage, it is useful not to bother with this at early design stages. To this end, BDL supports a flexible, dual synchronous/asynchronous semantics for its communications. It provides sounded support for moving from synchronous to asynchronous communication while preserving dynamic semantics. We illustrate the use of BDL on a small example of service adaptation in telecommunications.

F. Jimenez-Fraustro, E. Rutten.
Modélisation synchrone de standards de programmation de systèmes de contrôle : le langage ST.  Revue de l'électricité et de l'électronique (SEE), (3):60--68, Mars 2000.
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.

H. Marchand, S. Pinchinat.
Supervisory Control Problem using Symbolic Bisimulation Techniques.  2000 American Control Conference, pages 4067--4071, Chicago, Illinois, USA, Juin 2000. (postscript)
Résumé : In this paper, we present methods for solving the basic Supervisory Control Problem (SCP) using algorithms based on bisimulation techniques. Barrett and Lafortune first presented the relations between bisimulation and controllability and provided algorithms for solving the SCP. We efficiently solve the same problem using Intensional Labeled Transition System (ILTS), an implicit representation of automaton, relying on algebraic methods.

H Marchand, O. Boivineau, S. Lafortune.
On the Synthesis of Optimal Schedulers in Discrete Event Control Problems with Multiple Goals.  SIAM Journal on Control and Optimization, 39(2):512--532, 2000.
Résumé : This paper deals with a new type of optimal control for Discrete Event Systems. Our control problem extends the theory of [sengupta98], that is characterized by the presence of uncontrollable events, the notion of occurrence and control costs for events, and a worst-case objective function. A significant difference with [sengupta98] is that our aim is to make the system evolve through a set of multiple goals, one by one, with no order necessarily pre-specified, whereas the previous theory only deals with a single goal. Our solution approach is divided into two steps. In the first step, we use the optimal control theory in [sengupta98] to synthesize individual controllers for each goal. In the second step, we develop the solution of another optimal control problem, namely, how to modify if necessary and piece together, or schedule, all of the controllers built in the first step in order to visit each of the goals with least total cost. We solve this problem by defining the notion of a scheduler and then by mapping the problem of finding an optimal scheduler to an instance of the well-known Traveling Salesman Problem (TSP). We finally suggest various strategies to reduce the complexity of the TSP resolution while still preserving global optimality.

H. Marchand, P. Bournai, M. Le Borgne, P. Le Guernic.
Synthesis of Discrete-Event Controllers based on the Signal Environment.  Discrete Event Dynamic System: Theory and Applications, 10(4):325-346, Octobre 2000.
Résumé : In this paper, we present the integration of controller synthesis techniques in the Signal environment through the description of a tool dedicated to the incremental construction of reactive controllers. The plant is specified in Signal and the control synthesis is performed on a logical abstraction of this program, named polynomial dynamical system (PDS) over Z/3Z= {-1,0,+1

H. Marchand, M. Samaan.
Incremental Design of a Power Transformer Station Controller using Controller Synthesis Methodology.  IEEE Transaction on Software Engineering, 26(8):729--741, Août 2000.
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, ... properties, as well as partial order relations to be checked by the plant. The control objectives equations are synthesized using algebraic transformations.

H Marchand, O. Boivineau, S. Lafortune.
Optimal control of discrete event systems under partial observation.  Rapport de Recherche CGR-00-10, Control Group, College of Engineering, University of Michigan, USA, Septembre 2000. (postscript)
Résumé : We are interested in a new class of optimal control problems for Discrete Event Systems (DES). We adopt the formalism of supervisory control theory [ramadge89 and model the system as the marked language generated by a finite state machine (FSM). Our control problem follows the theory in [sengupta98] and is characterized by the presence of uncontrollable events, the notion of occurrence and control costs for events and a worst-case objective function. However, compared to the work in [sengupta98], we wish to take into account partial observability. Our solution approach consists of two steps. The first step is the derivation of an observer for the partially unobservable FSM, called a C-observer, which allows us to mask the underlying nondeterminism and to construct an approximation of the unobservable trajectory costs. We then define the performance measure on this observer rather than on the original FSM itself. In the second step, we use the algorithm presented in [sengupta98] to synthesize an optimal submachine of the C-observer. This submachine leads to the desired supervisor for the system.

H. Marchand, E. Rutten, M. Le Borgne, M. Samaan.
Formal Verification of SIGNAL programs: Application to a Power Transformer Station Controller.  Science of Computer Programming, 2000.
Résumé : We present a formal specification and verification of the automatic circuit-breaking behavior of an electric power transformer station, using the synchronous approach to reactive real-time systems implemented by the data-flow language Signal. Synchronous languages have a mathematical model that supports the various phases of the development of a control system: specification, verification, simulation, code generation, and implementation. The complex hierarchical, state-based and preemptive behavior of the power station controller is specified in Signalgti, an extension of Signal with notions of time intervals and preemptive tasks. To validate the specification, a graphical simulator is generated using Signal's execution environment, and the required behaviour is proven to be satisfied, using its proof method.

S. Pinchinat, H. Marchand.
Symbolic Abstractions of Automata.  Proc of 5th Workshop on Discrete Event Systems, WODES 2000, pages 39--48, Ghent, Belgium, Août 2000. (postscript)
Résumé : 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 introduce other kinds of abstraction, falling into the category of abstraction by restriction: in particular, we study the use of the controller synthesis methodology to achieve the restriction synthesis.

Y. Wang, J.P. Talpin, A. Benveniste, P. Le Guernic.
A semantics of UML state-machines using synchronous pre-order transition systems.  International Symposium on Object-Oriented Real-Time Distributed Computing (ISORC'2000), IEEE Press, Mars 2000. (postscript)
Résumé : The synchronous model of concurrency has demonstrated its practicality for the design of circuits, embedded systems, reactive and distributed systems. This model allows to design systems around an idealized notion of deterministic concurrency, which is much easier to deal with than classical, nondeterministic, asynchronous concurrency. Compiling, optimizing, and verifying programs are done using powerful techniques. We take advantage of this rich background by presenting a translation of UML state-machines into a pivot synchronous calculus, based on mathematical notions of pre-orders, in the aim of providing an integrated development cycle for the reliable deployment of synchronous system specifications over asynchronous networks. In this paper, we first present the structure of UML state-machines. Compared with earlier studies on that matter, the structure under consideration supports, e.g., composite transition and history. Then, we give a brief presentation of the pivot formalism, BDL, which is used to finally give a formal semantics of UML state-machine in terms of pre-ordered transition systems.

J.P Talpin.
Synchronous modeling and asynchronous deployment of mobile processes.  Rapport de Recherche Irisa, No1305, Mars 2000. (postscript)
Résumé :
We introduce the programming model consisting of pre-ordered transition systems (Spots) for modeling synchronous and asynchronous concurrent systems in the presence of mobility and of dynamicity. The model of Spots provides an operational and a denotational semantics to an expressive calculus of mobile processes. Encodings of related asynchronous, synchronous and functional calculi (Join, Fusion and ^$\lambda$^ ) are provided. The data-structure of Spots is shown to have a canonical, hierarchic, representation. This representation is the basis for the decisions of key properties for a correct deployment of synchronous system specifications on asynchronous architecture. The property of endochrony (i.e. the equivalence between the synchronous (internal) and asynchronous (external) observation of a system) determines which components of a system can be compiled separately and executed autonomously; The property of isochrony (i.e. the equivalence between the synchronous and asynchronous compositions of endochronous components) determines which components of a system can be distributed over a network without loss of information. Keywords: Concurrency, synchrony and asynchrony, mobile processes

Y. Wang, J.P. Talpin, A. Benveniste, P. Le Guernic.
Pre-order semantics of UML state machines.  Rapport de Recherche Irisa, No1336, Juin 2000. (postscript)
Résumé : The concept of synchronous programming has been proposed and widely accepted in the design of real-time systems, circuits, and embedded systems. Some recent researches have also proposed a mechanism to distribute a synchronous system over asynchronous networks. Meanwhile, UML is also becoming a standard framework of object-oriented methodologies. Our research aims to take advantage of these rich backgrounds by integrating a synchronous pivot called SPOTS (synchronous pre-order transition system) into UML and to propose a new methodology for the development of real-time distributed systems. In this paper, we focus on the issue of UML state-machines. We first present a recursive structure of UML state-machines. Compared with earlier studies, this structure supports composite transitions and histories. After a brief introduction to the pivot SPOTS, we will concentrate on the formal semantics of UML state machine by translating it in SPOTS. We will also give some complete examples of the translation according to the prototype we have implemented.

P. Le Maigat, L. Helouet.
A (max,+) Approach for time in Message Sequence Charts.  Workshop on DES, WODES'00, pages 83--92, Ghent, Belgium, Août 2000. (postscript)
Résumé : This paper details an approach for studying time in Message Sequence Charts (MSCs). MSCs are first transformed into order automata, and then into (max,+) automata, which allows for the use of well known (max,+) techniques.

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