@INPROCEEDINGS{beauvais99a,
  AUTHOR =	 {Beauvais, J.R. and Houdebine, R. and Tang, Y.M. and {Le
                  Guernic}, P. and Rutten, E. and Gautier, T.},
  BOOKTITLE =	 {Actes du 2ème Congrès sur la Modélisation des Systèmes
                  Réactifs, MSR'99},
  ADDRESS =	 {Cachan},
  MONTH =	 mars,
  CONFNAT =	 true,
  TITLE =	 {Une modélisation de StateCharts et ActivityCharts en Signal},
  YEAR =	 {1999},
  THEME =	 {stm},
  URL =		 {ftp://ftp.irisa.fr/local/signal/publis/articles/MSR-99:stm.ps.gz}
  ABSTRACT = { 
Cet article décrit une modélisation des langages de \statemate~:
Statecharts (qui est impératif) et Activitycharts,
dans le langage déclaratif équationel Signal. 
Cette modélisation fournit une traduction qui 
rend possible la spécification multi-formalisme,
et fournit un support à l'interopérabilité des langages.
Elle donne accès depuis une spécification en Statemate  
au format d'échange Dc+ (proche de Signal),
défini comme support d'échanges entre les outils 
mettant en oeuvre la technologie synchrone.
De là, on a accès à
des fonctionnalités de vérification, validation, compilation, 
optimisation, génération de code efficace et compact,
éventuellement distribué ou dépendant de l'architecture 
d'exécution.

<br>

<b> Keywords: </b>

        
}
}

@PHDTHESIS{beauvais99b,
  AUTHOR =	 {Beauvais, J.R.},
  TITLE =	 {Modélisation de StateCharts en Signal pour la conception de
                  systèmes critiques temps-réel},
  SCHOOL =	 {Université de Rennes 1, IFSIC},
  MONTH =	 janvier,
  YEAR =	 {1999},
  URL =		 {ftp://ftp.irisa.fr/techreports/theses/1999/beauvais.ps.gz}
  ABSTRACT = { 
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.
<br>

<b> Abstract </b>:
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.

        
}
}

@Article{benveniste99a,
  author = 	 {Benveniste, A.  and Caillaud, B. and {Le Guernic}, P.},
  title = 	 {Compositionality in dataflow synchronous languages: specification & distributed code generation},
  journal = 	 {Information and Computation},
  year = 	 {1999},
  note = 	 {(To appear)}
}

@InProceedings{benveniste99b,
  author = 	 {Benveniste, A.  and Caillaud, B. and {Le Guernic}, P.},
  title = 	 {From synchrony to asynchrony.},
  booktitle = 	 {CONCUR'99, Concurrency Theory, 10th International Conferenc, Volume 1664 of LNCS},
  pages = 	 {162-177},
  year = 	 {1999},
  editor = 	 {Baeten, {J.C.M.} and Mauw, S.},
  month = 	 {August},
  publisher = {Springer Verlag}
}

@TECHREPORT{benveniste99c,
  AUTHOR = 	 {Benveniste, A. and Caspi, P.},
  TITLE = 	 {Distributing synchronous programs on a loosely synchronous, distributed architecture},
  INSTITUTION =  {Irisa},
  YEAR = 	 {1999},
  NUMBER = 	 {1289},
  MONTH = 	 decembre,
  URL =		 {ftp://ftp.irisa.fr/techreports/1999/PI-1289.ps.gz}
  ABSTRACT = {   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.

<br>

<b>  Keywords:</b> Synchronous  languages, desynchronization,  distributed code
generation, loosely synchronous.


        
}
}

@TECHREPORT{benveniste99d,
  AUTHOR = 	 {Benveniste, A.  and Caillaud, B. and {Le Guernic}, P.},
  TITLE = 	 {From synchrony to asynchrony.},
  INSTITUTION =  {Irisa},
  YEAR = 	 {1999},
  NUMBER = 	 {1233},
  MONTH = 	 mars,
  URL =		 {ftp://ftp.irisa.fr/techreports/1999/PI-1233.ps.gz}
  ABSTRACT = {   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.

<br>

<b>  Keywords:</b> Synchronous languages, desynchronization 


        
}
}


@INPROCEEDINGS{besnard99,
  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 =	 {Proceedings of The 12th International Symposium on Languages
                  for Intensional Programming, ISLIP' 99},
  DATE =	 {28--30},
  MONTH =	 juin,
  ADDRESS =	 {NCSR Demokritos, Athens, Greece},
  YEAR =	 {1999},
  URL =		 {ftp://ftp.irisa.fr/local/signal/publis/articles/ISLIP-99: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. 

<br>
        
}
}


@INPROCEEDINGS{besson99a,
  AUTHOR =	 {Besson, F. and Jensen, T. and Talpin, J.-P.},
  TITLE =	 {Timed polyhedra analysis for synchronous languages},
  BOOKTITLE =	 {Proceedings of the 10th International Conference on
                  Concurrency Theory (CONCUR'99), LNCS volume 1664},
  MONTH =	 {August},
  YEAR =	 {1999},
  PUBLISHER =	 {Springer Verlag}
  URL =		 {ftp://ftp.irisa.fr/local/signal/publis/articles/CONCUR99-besson.ps.gz}
}

@INPROCEEDINGS{gautier99a,
  AUTHOR =	 {Gautier, T. and {Le Guernic}, P. },
  TITLE =	 {Code generation in the SACRES project},
  BOOKTITLE =	 {Towards System Safety, Proceedings of the Safety-critical
                  Systems Symposium, SSS'99},
  MONTH =	 fevrier,
  DATE =	 {9--11},
  PUBLISHER =	 {Springer},
  ADDRESS =	 {Huntingdon, UK},
  YEAR =	 {1999},
  THEME =	 {format,dist},
  URL =		 {ftp://ftp.irisa.fr/local/signal/publis/articles/SSS-99:format_dist.ps.gz}
  ABSTRACT = {  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.

<br>

<b> Keywords: </b>

        
}
}

@INPROCEEDINGS{jimenez99a,
        AUTHOR          = {Jiménez, F. and Rutten, E.},
        TITLE           = {A synchronous model of the PLC programming language ST},
        BOOKTITLE       = {Proceedings of the Work In Progress session, 11th Euromicro Conference on Real Time Systems, ERTS'99},
        ADDRESS         = {York, England},
        MONTH           = juin,
        DATE            = {9--11},
        PAGES           = {21--24},
        YEAR            = 1999,
        URL = {ftp://ftp.irisa.fr/local/signal/publis/articles/ecrts99-wip.ps.gz}
        ABSTRACT = {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. }
}


@INPROCEEDINGS{jimenez99b,
        AUTHOR          = {Jiménez, F.  and Rutten, E.},
        TITLE           = {Modélisation synchrone de standards de programmation de systèmes de contrôle},
        BOOKTITLE       = {Actes de la  Journée d'études sur les Nouvelles Percées dans les Langages pour l'Automatique},
        YEAR            = 1999,
        ADDRESS         = {Amiens},
        MONTH           = novembre,
        CONFNAT         = true,
        DATE            = {25},
        URL = {ftp://ftp.irisa.fr/local/signal/publis/articles/jsee99.ps.gz}
        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.  }
}

@TechReport{kerboeuf99a,
  author =	 {Kerboeuf, M. and Nowak, D. and Talpin, J.-P.},
  title =	 {The steam-boiler problem in SIGNAL-COQ},
  INSTITUTION =	 {Irisa / Inria-Rennes},
  YEAR =	 {1999},
  number =	 {3773},
  month =	 {October},
  URL =		 {ftp://ftp.inria.fr/INRIA/publication/publi-ps-gz/RR/RR-3773.ps.gz}
  ABSTRACT = {  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.  <br>

<b>  Keywords:</b> Reactive Systems / Synchronous Model / Verification / Model
Checking / Proof Assistant / Co-Induction 

        
}
}

@INPROCEEDINGS{kountouris99a,
  AUTHOR =	 {Kountouris, A. and Wolinski, C. },
  BOOKTITLE =	 {12th International Conference on VLSI Design},
  ADDRESS =	 {Goa, India},
  MONTH =	 janvier,
  TITLE =	 {Hierarchical Conditional Dependency Graphs for Mutual Exclusiveness Identification},
  DATE =	 {7-10},
  YEAR =	 {1999}
}

@INPROCEEDINGS{kountouris99b,
  AUTHOR =	 {Kountouris, A. and Wolinski, C. },
  BOOKTITLE =	 {ASP-DAC'99},
  ADDRESS =	 {Hong Kong},
  MONTH =	 janvier,
  TITLE =	 {Combining Speculative Execution and Conditional Resource  Sharing to Efficiently Schedule Conditional Behaviors},
  YEAR =	 {1999}
}

@INPROCEEDINGS{kountouris99c,
  AUTHOR =       {Kountouris, A. and Wolinski, C.},
  BOOKTITLE =    {Proceedings of the EUROMICRO'99},
  PUBLISHER =    {IEEE Computer Society Press},
  ADDRESS =      {Milan, Italie},
  MONTH =        aout,
  TITLE =        {High-level Pre-synthesis Optimization Steps using Hierarchical Conditional Dependency Graphs},
  YEAR =         {1999}
}

@INPROCEEDINGS{lelann99a,
  AUTHOR =	 {{Le Lann}, {J.C.} and Wolinski, C. },
  BOOKTITLE =	 {Proceedings of the SCI'99/ISAS'99},
  ADDRESS =	 {Orlando, Floride},
  MONTH =	 aout,
  TITLE =	 {Load Balancing and Functional Unit Assignment in High-Level Synthesis.},
  YEAR =	 {1999}
}

@INPROCEEDINGS{marchand99a,
  AUTHOR =	 {Marchand, H. and Samaan, M.},
  TITLE =	 {On the Incremental Design of a Power Transformer Station
                  Controller using Controller Synthesis Methodology},
  BOOKTITLE =	 {World Congress on Formal Methods (FM'99), Volume 1709 of LNCS},
  YEAR =	 {1999},
  ADDRESS =	 {Toulouse, France},
  MONTH =	 {October},
  PAGES =	 {1605-1624},
  DATE =	 {20-24},
  URL =		 {ftp://ftp.irisa.fr/local/signal/publis/articles/FM99:control_synth_appli.ps.gz}
  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,   attractivity
  properties, as  well as partial order  relations to be checked  by the plant.
  The  control  objectives  equations  are  then  synthesized  using  algebraic
  transformations.

<br>

<b> Keywords: </b>
Discrete Event Systems, Polynomial Dynamical System, Supervisory Control
Problem, \signal, Power Plant.

        
}
}

@TechReport{marchand99b,
  author =	 {Marchand, H. and {Le Borgne}, M.},
  title =	 {The Supervisory Control Problem of Discrete Event Systems using polynomial Methods},
  INSTITUTION =	 {Irisa},
  YEAR =	 {1999},
  number =	 {1271},
  month =	 {October},
  URL =		 {ftp://ftp.irisa.fr/techreports/1999/PI-1271.ps.gz}
  ABSTRACT = {  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}
  or the {\it reachability} of a given  set of states, as well as partial order
  relation to be checked by the controlled plant.

<br>

<b> Keywords:</b> Discrete Event Systems, Polynomial Dynamical Systems,  Supervisory Control Problem, Optimal
  Control, Polynomial Methods.


        
}
}




@INPROCEEDINGS{nowak99a,
  AUTHOR =	 {Nowak, D. and Talpin, J.P. and {Le Guernic}, P.},
  TITLE =	 {Synchronous Structures},
  BOOKTITLE =	 {Proceedings of the 10th International Conference on
                  Concurrency Theory (CONCUR'99), Volume 1664 of LNCS},
  MONTH =	 {August},
  YEAR =	 {1999},
  PUBLISHER =	 {Springer Verlag},
  URL =		 {ftp://ftp.irisa.fr/local/signal/publis/articles/TPHOLs-98:sem_verif.ps.gz}
  ABSTRACT = {  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.  <br>

<b>  Keywords: </b>  reactive systems,  synchronous programming,  order theory,
category theory.

        
}
}

@PHDTHESIS{nowak99b,
  author =	 {Nowak, D.},
  title =	 {Spécification et preuve de systèmes réactifs},
  school =	 {Université de Rennes 1, IFSIC},
  month =	 {October},
  year =	 {1999},
  URL =		 {ftp://ftp.irisa.fr/techreports/theses/1999/nowak.ps.gz}
  ABSTRACT = { 
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).
<br>
<b> Mots   clefs </b> :   Programmation synchrone,  outil  d'aide à la
preuve, structure synchrone. 
<br>


 
<b>  Abstract  </b>: 

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).


  <br>

<b>  Keywords: </b>  Synchronous programming, proof assistant, synchronous structure.

        
}
}

@TECHREPORT{pinchinat99,
  AUTHOR = 	 {Pinchinat, S. and  Marchand, H. and  {Le Borgne}, M.},
  TITLE = 	 {Symbolic Abstractions of Automata and their application to the Supervisory Control Problem},
  INSTITUTION =	 {Irisa},
  YEAR = 	 {1999},
  NUMBER = 	 {1279},
  MONTH = 	 novembre,
  URL =		 {ftp://ftp.irisa.fr/techreports/1999/PI-1279.ps.gz}
  ABSTRACT = {   

In this report, we describe the design of abstraction methods based on symbolic
  techniques: classical <b>abstraction by state fusion</b> has been considered.
  we present a general method to abstract  automata on the basis of a <i> state
  fusion  criterion</i>,  derived from  e.g.   equivalence  relations (such  as
  bisimulation),   partitions,  ...    We  also   introduced  other   kinds  of
  abstraction, falling  into the category of <b>abstraction by restriction</b>:
  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.  <br>

<b>  Keywords: Intentional transition systems, polynomials, symbolic bisimulations,
  model reduction, BDD, Supervisory control Problem</b> 

        
}
}

@MISC{pinchinat99b,
  AUTHOR   = {  Pinchinat, S. and  Marchand, H.   and {Le Borgne}, M. },
  TITLE   = {Deliverable  3.1.3: Symbolic Abstractions  of Automata and  their application to  the Supervisory Control Problem},
  BOOKTITLE    = {Esprit project 22703: Syrf},
  MONTH    = octobre,
  YEAR  = {1999}
}

@INPROCEEDINGS{smarandache99a,
  AUTHOR =	 {Smarandache, I. and Gautier, T. and {Le Guernic}, P.},
  TITLE =	 {Validation of Mixed Signal-Alpha Real-Time Systems through
                  Affine Calculus on Clock Synchronisation Constraints.},
  BOOKTITLE =	 {World Congress on Formal Methods (FM'99), Volume 1709 of LNCS},
  YEAR =	 {1999},
  ADDRESS =	 {Toulouse, France},
  MONTH =	 {October},
  DATE =	 {20-24},
  PAGES =	 {1364-1383},
  URL =		 {ftp://ftp.irisa.fr/local/signal/publis/articles/FM-99:affine.ps.gz}
  ABSTRACT = { 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.

<br>
        
}
}


@TechReport{talpin99a,
  author =	 {Talpin, {J.-P.} and  Benveniste, A. and  {Le Guernic}, P.},
  title =	 {Asynchronous deployment of synchronous transition systems},
  INSTITUTION =	 {Irisa},
  YEAR =	 {1999},
  number =	 {1269},
  month =	 {October},
  URL =		 {ftp://ftp.irisa.fr/techreports/1999/PI-1269.ps.gz}
  ABSTRACT = {  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.  <br>

<b>    Keywords:   </b>    Synchronous    programming,   transition    systems,
desynchronization, compilation

        
}
}


@TechReport{talpin99b,
  author =	 {Talpin, {J.-P.} and  Benveniste, A. and Caillaud, B. and  {Le Guernic}, P.},
  title =	 {Hierarchic Normal Forms for desynchronization},
  INSTITUTION =	 {Irisa},
  YEAR =	 {1999},
  number =	 {1288},
  month =	 decembre,
  URL =		 {ftp://ftp.irisa.fr/techreports/1999/PI-1288.ps.gz}
  ABSTRACT = {  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.  <br>

<b>    Keywords:   </b>  Synchronous languages, desynchronization, distributed code generation
        
}
}



@TechReport{tudoret99,
  author =	 {Tudoret, S.},
  title =	 {Signal-Simulink : Hybrid System Co-simulation},
  INSTITUTION =	 {Linköping},
  YEAR =	 {1999},
  number =	 {20},
  month =	 decembre,
  URL =		 {http://www.ep.liu.se/ea/cis/1999/020/}
  ABSTRACT = {  

<br>

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.

        
}
}


@PHDTHESIS{rutten99a,
        AUTHOR          = {Rutten, E.},
        SCHOOL          = {Ifsic, Université de Rennes1},
        TITLE           = {Programmation  sûre des systèmes de contrôle/commande: le séquencement de tâches flot de données dans les langages réactifs},
HDR = true,
        MONTH           = decembre,
        Year            = 1999,
        URL = {ftp://ftp.irisa.fr/techreports/habilitations/rutten.ps.gz}
}