@InCollection{besnard00a,
AUTHOR = {Besnard, L. and Bournai, P. and Gautier, T. and Halbwachs, N. and {Nadjm-Tehrani}, S. and Ressouche, A.},
TITLE = {Design of a Multi-formalism Application and Distribution in a Data-flow Context: An Example},
BOOKTITLE = {Intensional Programming II, Based on the Papers at ISLIP '99},
PUBLISHER = {World Scientific},
YEAR = {2000},
EDITOR = {Gergatsoulis, M. and Rondogiannis, P.},
pages = {149--167},
YEAR = {2000},
URL= {ftp://ftp.irisa.fr/local/signal/publis/articles/IP2-00:appli_format_dist.ps.gz}
ABSTRACT ={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.}
}
@TechReport{caillaud00a,
author = {Caillaud, B. and Talpin, J. P. and Jezequel, J. M. and Benveniste, A. and Jard, C.},
title = {BDL: a semantics backbone for UML dynamic diagrams},
INSTITUTION = {Inria},
YEAR = {2000},
NUMBER = {4003},
month = septembre,
URL = {ftp://ftp.inria.fr/INRIA/publication/publi-ps-gz/RR/RR-4003.ps.gz}
ABSTRACT = {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. }
}
@MISC{gautier00a,
AUTHOR = {Gautier, T. and {Le Guernic}, P.},
TITLE = {SCADE--SIGNAL languages Compatibility},
NOTE = {Advanced Design Tools for Aircraft Systems and Airborne
Software (SafeAir)},
MONTH = mai,
YEAR = {2000}
}
@INPROCEEDINGS{helouet00a,
AUTHOR = {Helouet, L. and {Le Maigat}, P.},
BOOKTITLE = {Workshop on SDL and MSC, SAM'00},
TITLE = {Decomposition of Message Sequence Charts},
YEAR = {2000},
pages = {47--60}
URL ={ftp://ftp.irisa.fr/local/signal/publis/articles/sam00_final.ps.gz}
}
@InProceedings{jimenez00a,
Author = {{Jimenez-Fraustro}, F. and Rutten, E.},
Title = {Hybrid simulation of IEC-61131 PLC programs using Signal and Simulink},
Booktitle = {Proceedings of the 4th International Conference on Automation of Mixed Processes, ADPM'00, 18-19 September 2000, Dortmund, Germany},
Year = 2000,
Pages = {171--176}
}
@ARTICLE{jimenez00a,
Author = {{Jimenez-Fraustro}, F. and Rutten, E.},
Title = {Modélisation synchrone de standards de programmation de systèmes de contrôle : le langage {ST} de la norme {CEI} 1131-3},
Journal = {Revue de l'électricité et de l'électronique (SEE)},
Number = {3},
Pages = {60--68},
Month = mars,
YEAR = 2000,
ABSTRACT = { 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.}
}
@INPROCEEDINGS{kerboeuf00a,
AUTHOR = {Kerboeuf, M. and Nowak, D. and Talpin, J. P.},
TITLE = {The steam-boiler problem in SIGNAL-COQ},
BOOKTITLE = {International Conference on Theorem Proving in Higher-Order
Logics},
MONTH = aout,
YEAR = {2000},
SERIES = {Lecture Notes in Computer Science},
PUBLISHER = {Springer},
URL = {ftp://ftp.irisa.fr/local/signal/publis/articles/paper_TPHOLs.ps.gz}
}
@INPROCEEDINGS{kountouris00a,
AUTHOR = {Kountouris, A. and Wolinski, C.},
TITLE = {Efficient Scheduling of Conditional Behaviors Using Hierarchical Conditional Dependency Graphs in CODESIS System},
BOOKTITLE = {Proceedings of EUROMICRO'00},
PUBLISHER = {IEEE Computer Society Press},
MONTH = septembre,
YEAR = {2000},
PAGES = {222--229},
ADDRESS = {Maastricht, The Netherlands},
}
@INPROCEEDINGS{kountouris00b,
AUTHOR = {Kountouris, A. and Wolinski, C.},
TITLE = {Hierarchical Conditional Dependency Graphs as a Unifying Design Representation in the CODESIS High-Level Synthesis System},
BOOKTITLE = {Proceedings of ISSS'00},
PUBLISHER = {IEEE Computer Society Press},
MONTH = septembre,
YEAR = {2000},
PAGES = {66--71},
ADDRESS = {Madrid, Spain},
}
@ARTICLE{kountouris00c,
AUTHOR = {Kountouris, A. and Wolinski, C. and {Le Lann}, {J.C.} },
TITLE = {High-Level Synthesis Using Hierarchical Conditional Dependency Graphs in the CODESIS System},
JOURNAL = {EUROMICRO Journal of Systems Architecture on Modern Methods and Tools in Digital System Design},
YEAR = {2000},
note = {à paraître}
}
@MISC{lesergent00a,
AUTHOR = {{Le Sergent}, T. and Camus, J. L. and Dupont, F. and Gautier, T. and {Le Guernic}, P. and Hungar, H. and Winkelmann, K. and Shtrichman, O. and Cohen, M.},
TITLE = {ASDE V0.9 specification},
NOTE = {Advanced Design Tools for Aircraft Systems and Airborne Software (SafeAir)},
MONTH = juin,
YEAR = {2000}
}
@INPROCEEDINGS{marchand00a,
AUTHOR = {Marchand, H. and Pinchinat, S.},
TITLE = {Supervisory Control Problem using Symbolic Bisimulation Techniques},
BOOKTITLE = {2000 American Control Conference},
DATE = {28--30},
MONTH = juin,
PAGES = {4067--4071},
YEAR = {2000},
ADDRESS = {Chicago, Illinois, USA},
URL = {ftp://ftp.irisa.fr/local/signal/publis/articles/ACC2000.ps.gz}
ABSTRACT = {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. }
}
@ARTICLE{marchand00b,
AUTHOR = {Marchand, H and Boivineau, O. and Lafortune, S.},
TITLE = {On the Synthesis of Optimal Schedulers in Discrete Event Control Problems with Multiple Goals},
JOURNAL = {SIAM Journal on Control and Optimization},
YEAR = {2000},
VOLUME = {39},
NUMBER = {2},
PAGES = {512--532},
ABSTRACT = {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. }
}
@ARTICLE{marchand00c,
AUTHOR = {Marchand, H. and Bournai, P. and {Le Borgne}, M. and {Le Guernic}, P.},
TITLE = {Synthesis of Discrete-Event Controllers based on the Signal Environment},
JOURNAL = {Discrete Event Dynamic System: Theory and Applications},
YEAR = {2000},
VOLUME = {10},
NUMBER = {4},
PAGES = {325-346},
MONTH = october,
ABSTRACT = {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}. The control of the plant is performed by
restricting the controllable input values with respect
to the control objectives. These restrictions are
obtained by incorporating new algebraic equations into
the initial system. This theory sets the basis for the
verification and the controller synthesis tool, Sigali.
Moreover, we present a tool developed around the Signal
environment allowing the visualization of the
synthesized controller by an interactive simulation of
the controlled system. In a first stage, the user
specifies in Signal both the physical model and the
control objectives to be ensured. A second stage is
performed by the Signal compiler which translates the
initial Signal program into a PDS, and the control
objectives in terms of polynomial relations/operations.
The controller is then synthesized using Sigali. The
result is a controller coded by a polynomial and then by
a Ternary Decision Diagram (TDD). Finally, in a third
stage, the obtained controller and some simulation
processes are automatically included in the initial
Signal program. It is then sufficient for the user to
compile the resulting Signal program which generates
executable code ready for simulation. Different
academic examples are used to illustrate the application
of the tool. }
}
@ARTICLE{marchand00d,
AUTHOR = {Marchand, H. and Samaan, M.},
TITLE = {Incremental Design of a Power Transformer Station Controller using Controller Synthesis Methodology},
JOURNAL = {IEEE Transaction on Software Engineering},
YEAR = {2000},
VOLUME = {26},
NUMBER = {8},
PAGES = {729--741},
MONTH = aout,
ABSTRACT = {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. }
}
@TECHREPORT{marchand00e,
AUTHOR = {Marchand, H and Boivineau, O. and Lafortune, S.},
TITLE = {Optimal control of discrete event systems under partial observation},
INSTITUTION = {CGR-00-10, Control Group, College of Engineering, University of Michigan, USA},
MONTH = septembre,
YEAR = {2000},
ABSTRACT = {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.},
URL = {ftp://ftp.irisa.fr/local/signal/publis/research_reports/RR-UoM.ps.gz},
}
@Article{marchand00g,
author = {Marchand, H. and Rutten, E. and {Le Borgne}, M. and Samaan, M.},
title = {Formal Verification of SIGNAL programs: Application to a Power Transformer Station Controller},
journal = {Science of Computer Programming},
year = {2000},
ABSTRACT = {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.},
note = {à paraître}
}
@INPROCEEDINGS{nebut00a,
AUTHOR = {Nebut, M.},
TITLE = {Calcul d'horloges et valeurs},
BOOKTITLE = {MOVEP'2k MOdelling and VErification of Parallel processes},
PUBLISHER = {École Centrale de Nantes},
editor = {Cassez, F. and Jard, C. and Rozoy, B. and Ryan, M.},
pages = {199--202},
DATE = {19-23},
MONTH = juin,
CONFNAT = true,
YEAR = {2000},
ADDRESS = {Nantes}
}
@INPROCEEDINGS{pinchinat00a,
AUTHOR = {Pinchinat, S. and Marchand, H.},
TITLE = {Symbolic Abstractions of Automata},
BOOKTITLE = {Proc of 5th Workshop on Discrete Event Systems, WODES 2000},
YEAR = {2000},
PAGES = {39--48},
MONTH = aout,
ADDRESS = {Ghent, Belgium},
URL = {ftp://ftp.irisa.fr/local/signal/publis/articles/Wodes2000.ps.gz}
ABSTRACT = {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.}
}
@InProceedings{tudoret00a,
author = {Turodet, S. and Nadjm-Tehrani, S. and Benveniste, A. and Strömberg, J. E.},
title = {Co-simulation of Hybrid Systems: Signal-Simulink},
booktitle = {Proceedings of 6th international school and symposium on Formal Techniques in Real-time and Fault-tolerant Systems},
year = {2000},
series = {Lecture Notes in Computer Science},
month = septembre,
publisher = {Springer}
}
@INPROCEEDINGS{wang00a,
AUTHOR = {Wang, Y. and Talpin, J. P. and Benveniste, A. and {Le Guernic}, P.},
TITLE = {A semantics of UML state-machines using synchronous pre-order transition systems},
BOOKTITLE = {International Symposium on Object-Oriented Real-Time Distributed Computing (ISORC'2000)},
PUBLISHER = {IEEE Press},
MONTH = mars,
YEAR = {2000},
URL = {http://www.irisa.fr/prive/talpin/isorc00.ps.gz}
ABSTRACT = { 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.
}
}
@INPROCEEDINGS{wang00b,
AUTHOR = {Wang, Y. and Talpin, J. P. and Benveniste, A. and {Le Guernic}, P.},
TITLE = {Compilation and distribution of state machines using Spots},
BOOKTITLE = {16th IFIP World Computer Congress (WCC'2000)},
MONTH = aout,
YEAR = {2000}
}
@TECHREPORT{talpin00a,
AUTHOR = {Talpin, J.P}
TITLE = {Synchronous modeling and asynchronous deployment of mobile processes},
INSTITUTION = {Irisa},
YEAR = {2000},
NUMBER = {1305},
MONTH = mars,
URL = {ftp://ftp.irisa.fr/techreports/2000/PI-1305.ps.gz}
ABSTRACT = {
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
}
}
@TechReport{wang00c,
author = {Wang, Y. and Talpin, J. P. and Benveniste, A. and {Le Guernic}, P.},
title = {Pre-order semantics of UML state machines},
INSTITUTION = {Irisa},
YEAR = {2000},
NUMBER = {1336},
MONTH = juin,
URL = {ftp://ftp.irisa.fr/techreports/2000/PI-1336.ps.gz}
ABSTRACT = { 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. }
}
@INPROCEEDINGS{wang00d,
AUTHOR = {Wang, Y.},
TITLE = {Compilation of state-machines using Behavior Expression},
BOOKTITLE = {Workshop PhDOOS2000 in 14th European Conference on Object-Oriented Programming},
YEAR = {2000}
}
@INPROCEEDINGS{lemaigat00a,
AUTHOR = {{Le Maigat}, P. and Helouet, L.},
BOOKTITLE = {Proc of 5th Workshop on Discrete Event Systems, WODES 2000},
MONTH = aout,
ADDRESS = {Ghent, Belgium},
BOOKTITLE = {Workshop on DES, WODES'00},
TITLE = {A (max,+) Approach for time in Message Sequence Charts},
YEAR = {2000},
pages = {83--92},
URL = {ftp://ftp.irisa.fr/local/signal/publis/articles/wodes00_final.ps.gz},
ABSTRACT = {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.
}
}
@PhdThesis{wolinski00a,
Author = {Wolinski, C.},
School = {Ifsic, Université de Rennes 1},
Title = {Conception conjointe matériels/logiciels},
Type = {Habilitation à diriger des recherches},
Month = Septembre,
Year = 2000
}