inproceeding.bib

@comment{{This file has been generated by bib2bib 1.96}}
@comment{{Command line: ./bib2bib -oc selection -ob inproceeding.bib -c 'category : "intc"' mesPublications.bib}}
@inproceedings{emzivat-ITSC-17,
  address = {Yokohama, JAPAN},
  author = {Emzivat, Yrvann and  Guzman, Javier Ibanez and Martinet, Philippe and Roux, Olivier H.},
  booktitle = {IEEE 20th International Conference on Intelligent Transportation Systems (ITSC 2017)},
  title = {Adaptability of an Automated Driving System Facing Inherent Hazardous Areas of the Road Network},
  year = 2017,
  category = {intc}
}
@inproceedings{david-CONCUR-17,
  address = {Berlin, Germany},
  author = {Nicolas David and Claude Jard and Didier Lime and Olivier H. Roux},
  booktitle = {The 28th International Conference on Concurrency Theory (CONCUR 2017)},
  editor = {Roland Meyer and Uwe Nestmann},
  month = sep,
  publisher = {Dagstuhl Publishing},
  series = {LIPIcs},
  title = {Coverability Synthesis in Parametric Petri Nets},
  year = 2017,
  category = {intc}
}
@inproceedings{boucheneb-FORMATS-17,
  address = {Berlin, Germany},
  author = {Hanifa Boucheneb and Didier Lime and Baptiste Parquier and Olivier H. Roux and Charlotte Seidner},
  booktitle = {15th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS 2017)},
  editor = {Nestmann, Uwe and Wolter, Katinka},
  month = sep,
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  title = {Optimal Reachability in Cost Time Petri Nets},
  year = 2017,
  category = {intc}
}
@inproceedings{emzivat-IV-17,
  address = {Redondo Beach, USA},
  author = {Emzivat, Yrvann and  Guzman, Javier Ibanez and Martinet, Philippe and Roux, Olivier H.},
  booktitle = {IEEE Intelligent Vehicles Symposium (IV 2017)},
  month = jun,
  title = {Dynamic Driving Task Fallback for an Autonomous Vehicle whose Perception Module has Failed},
  year = 2017,
  category = {intc}
}
@inproceedings{andre-ICFEM-16,
  address = {Tokyo, Japan},
  author = {\'Etienne Andr\'e and Didier Lime and Olivier H. Roux},
  booktitle = {18th International Conference on Formal Engineering Methods (ICFEM 2016)},
  editor = {Ogata, Kazuhiro and Lawford, Mark and Liu, Shaoying},
  month = nov,
  volume = {10009},
  pages = {400--416},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  title = {Decision Problems for Parametric Timed Automata},
  year = 2016,
  category = {intc}
}
@inproceedings{parquier-FTSCS-16,
  address = {Tokyo, Japan},
  author = {Baptiste Parquier and Laurent Rioux and Rafik Henia and Romain Soulat and Olivier H. Roux and Didier Lime and \'Etienne Andr\'e},
  booktitle = {5th International Workshop on Formal Techniques for Safety-Critical Systems (FTSCS 2016)},
  editor = {Artho, Cyrille and Peter Csaba \"Olveczky},
  month = nov,
  publisher = {Springer},
  series = {Communications in Computer and Information Science},
  title = {Applying Parametric Model-checking Techniques for Reusing Real-time Critical Systems},
  year = 2016,
  category = {intc}
}
@inproceedings{andre-FORMATS-16,
  address = {Qu\'ebec City, Canada},
  author = {\'Etienne Andr\'e and Didier Lime and Olivier H. Roux},
  title = {On the Expressiveness of Parametric Timed Automata},
  booktitle = {14th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS 2016)},
  editor = {Martin Fr\"anzle and Nicolas Markey},
  month = aug,
  publisher = {Springer},
  pages = {19--34},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = {9984},
  year = 2016,
  category = {intc}
}
@inproceedings{emzivat-ICATPN-16,
  address = {Toru\'n, Poland},
  author = {Yrvann Emzivat and Beno\^it Delahaye and Didier Lime and Roux, Olivier H.},
  booktitle = {The 37th International Conference on Application and Theory of Petri Nets and Concurrency (Petri Nets 2016)},
  editor = {Fabrice Kordon and Daniel Moldt},
  month = jun,
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  title = {Probabilistic Time Petri Nets},
  volume = {9698},
  pages = {261--280},
  year = 2016,
  category = {intc}
}
@inproceedings{givel-SIES-16,
  author = {Louis{-}Marie Givel and  Jean{-}Luc B{\'{e}}chennec and Matthias Brun and  S{\'{e}}bastien Faucou and  Olivier H. Roux},
  title = {Testing real-time embedded software using runtime enforcement},
  booktitle = {11th {IEEE} Symposium on Industrial Embedded Systems, {SIES} 2016,
               Krakow, Poland, May 23-25, 2016},
  month = may,
  pages = {199--204},
  year = {2016},
  category = {intc}
}
@inproceedings{andre-RP-15,
  address = {Warsaw, Poland},
  author = {\'Etienne Andr\'e and Didier Lime and Olivier H. Roux},
  booktitle = {The 9th International Workshop on Reachability Problems},
  month = sep,
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = {9328},
  title = {Integer-Complete Synthesis for Bounded Parametric Timed Automata},
  pages = {7--19},
  year = 2015,
  category = {intc}
}
@inproceedings{tigori-ICESS-15,
  author = {Tigori, Kabland Toussaint Gautier and  Bechennec, Jean-Luc and and Roux, Olivier H.},
  title = { Formal Synthesis of Optimal RTOS},
  booktitle = {The 12th IEEE international Conference on Embedded Software and Systems },
  month = aug,
  year = 2015,
  organization = {IEEE},
  address = {New York, USA},
  category = {intc}
}
@inproceedings{givel-ICESS-15,
  title = {Use of runtime enforcement for the test of real-time systems},
  author = {Givel, Louis-Marie and Brun, Matthias and Constant, Camille and Faucou, Sebastien and Roux, Olivier H.},
  booktitle = {The 12th IEEE international Conference on Embedded Software and Systems },
  month = aug,
  year = {2015},
  organization = {IEEE},
  address = {New York, USA},
  category = {intc}
}
@inproceedings{david-ICATPN-15,
  address = {Brussels, Belgium},
  author = {Nicolas David and Claude Jard and Didier Lime and Olivier
H. Roux},
  booktitle = {The 36th International Conference on Application and Theory
of {{P}etri} Nets and Concurrency (ICATPN 2015)},
  editor = {Raymond Devillers and Antti Valmari},
  volume = {9115},
  pages = {137--156},
  month = jun,
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  title = {Discrete Parameters in {P}etri Nets},
  acceptrate = {40\%},
  year = 2015,
  category = {intc}
}
@inproceedings{girault-DCDS-15,
  author = {Girault, Johan and Loiseau, Jean-Jacques  and Roux, Olivier H. },
  title = {On-line optimal compositional controller synthesis for AGV by unfolding},
  booktitle = {5th international Workshop on Dependable Control of Discrete Systems (DCDS 2015)},
  address = {{C}ancun, {M}exico},
  year = 2015,
  category = {intc}
}
@inproceedings{tanguy-simultech-14,
  title = {Reactive Embedded Device Driver Synthesis using Logical Timed Models},
  author = {Tanguy, Julien and  B\'echennec, Jean-Luc and  Briday, Mika\"el  and Roux, Olivier H.},
  booktitle = {The 4th International Conference on Simulation and Modeling Methodologies, Technologies and Applications (SIMULTECH 2014)},
  publisher = {Scitepress Digital Library},
  address = {{V}ienna, {A}ustria },
  month = aug,
  year = {2014},
  category = {intc}
}
@inproceedings{jovanovic-ATVA-13,
  address = {Hanoi, Vietnam},
  author = {Jovanovi\'c, Aleksandra and Lime, Didier and  Roux, Olivier H.},
  booktitle = {The 11th International Symposium on Automated Technology for Verification and Analysis (ATVA 2013)},
  editor = {Hung Dang-Van and Mizuhito Ogawa},
  month = oct,
  publisher = {Springer},
  volume = {8172},
  series = {Lecture Notes in Computer Science},
  title = {Synthesis of Bounded Integer Parameters for Parametric Timed Reachability Games},
  year = 2013,
  pages = {87--101},
  pdf = {./fichiers/conf/jlr-atva-2013.pdf},
  category = {intc}
}
@inproceedings{lelionnais-VALID-13,
  title = { Formal Composition Based on Roles within a Model Driven Engineering Approach},
  author = {Lelionnais, C\'edrick  and Brun, Matthias and Delatour, J\'er\^ome  and Roux, Olivier H. and  Seidner, Charlotte },
  booktitle = {The 5th International Conference on Advances in System Testing and Validation Lifecycle (VALID 2013)},
  address = {Venice, {I}taly },
  year = {2013},
  category = {intc}
}
@inproceedings{tanguy-ETFA-13,
  title = { Device driver synthesis for embedded systems},
  author = {Tanguy, Julien and  B\'echennec, Jean-Luc and  Briday, Mika\"el  and Roux, Olivier H. and  Dub\'e, S\'ebastien},
  booktitle = {The 18th {IEEE} {I}nternational {C}onference on {E}merging {T}echnologies &{F}actory {A}utomation ({ETFA} 2013)},
  publisher = {{IEEE} {C}omputer {S}ociety },
  address = {{C}agliari, {I}taly },
  year = {2013},
  category = {intc}
}
@inproceedings{boucheneb-ICATPN-13,
  address = {Milano, Italy},
  author = {Hanifa Boucheneb and Didier Lime and Olivier H. Roux},
  booktitle = {The 34th International Conference on Application and Theory
of {{P}etri} Nets and other models of concurrency (ICATPN 2013)},
  editor = {Jos\'e Manuel Colom and J\"org Desel},
  month = jun,
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = {7927},
  pages = {130--149},
  title = {On Multi-enabledness in Time Petri Nets},
  acceptrate = {33\%},
  year = 2013,
  category = {intc}
}
@inproceedings{jovanovic-TACAS-13,
  address = {Roma, Italy},
  author = {Jovanovi\'c, Aleksandra and Lime, Didier and  Roux, Olivier H.},
  title = {Integer Parameter Synthesis for Timed Automata},
  booktitle = {19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2013)},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = {7795},
  pages = {401--415},
  editor = {Nir Piterman and Scott Smolka},
  month = mar,
  acceptrate = {24\%},
  year = 2013,
  note = {(See extended version in {IEEE TSE vol 41 issue 5, 2015})},
  category = {intc}
}
@inproceedings{lime-CSP-12,
  address = {Berlin, Germany},
  author = {Jard, Claude and Lime, Didier and  Roux, Olivier H},
  title = {{Clock Transition Systems}},
  booktitle = {21th international Workshop on Concurrency, Specification and Programming (CS\&P 2012)},
  month = sep,
  year = 2012,
  publisher = {Bia\lystok University of Technology, ISBN 978-83-62582-42-6},
  category = {intc}
}
@inproceedings{jovanovic-WODES-12,
  address = {Guadalajara, Mexico},
  author = {Jovanovi\'c, Aleksandra and Faucou, S\'ebastien and Lime, Didier and  Roux, Olivier H.},
  title = {{Real-Time Control with Parametric Timed Reachability Games}},
  booktitle = {11th International Workshop on Discrete Event Systems (WODES'12)},
  publisher = {IFAC},
  month = oct,
  year = 2012,
  url = {http://www.ifac-papersonline.net/Discrete_Event_Systems/11th_International_Workshop_on_Discrete_Event_Systems/index.html/},
  pages = {323-330},
  address = {Guadalajara, Mexico},
  category = {intc}
}
@inproceedings{boucheneb-WODES-12,
  address = {Guadalajara, Mexico},
  author = {Boucheneb, Hanifa and Bullich, Adrien and Roux, Olivier H.},
  title = {{FIFO Time Petri Nets for conflicts handling}},
  booktitle = {11th International Workshop on Discrete Event Systems (WODES'12)},
  publisher = {IFAC},
  month = oct,
  year = 2012,
  pages = {143-148},
  address = {Guadalajara, Mexico},
  url = {http://www.ifac-papersonline.net/Discrete_Event_Systems/11th_International_Workshop_on_Discrete_Event_Systems/index.html/},
  category = {intc}
}
@inproceedings{akshay-FORMATS-12,
  address = {London, UK},
  author = {Akshay, S and  H\'elou\"et, Lo\"ic  and Jard, Claude and Lime, Didier and  Roux, Olivier H.},
  title = {{Robustness of Time Petri Nets under architectural constraints}},
  booktitle = {10th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS 2012)},
  editor = {Marcin Jurdzinski and Dejan Nickovic},
  month = sep,
  volume = {7595},
  pages = {11--26},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  year = 2012,
  pdf = {./fichiers/conf/ahjlr-formats-2012},
  category = {intc}
}
@inproceedings{lelionnais-DDIS-12,
  author = {Lelionnais, Cedric and  Brun, Matthias and Delatour, Jerome and Roux, Olivier H. and Seidner,  Charlotte},
  title = {Formal Behavioral Modeling of Real-Time Operating Systems},
  booktitle = {14th Int. Conf. Ent. Information Systems - Model Driven Development for Information Systems (MDDIS 2012), },
  year = 2012,
  month = june,
  address = {Wroclaw, Poland},
  category = {intc}
}
@inproceedings{bullich-CITSA-12,
  author = {  Bullich, Adrien and Boucheneb, Hanifa and Roux, Olivier H.},
  title = {Refinement of time {Petri} nets semantics in conflict situations},
  booktitle = {The 9th International Conference on Cybernetics and Information Technologies, Systems and Applications: CITSA 2012 },
  year = 2012,
  month = jul,
  address = {Orlando, USA},
  category = {intc}
}
@inproceedings{bennatar-AFL-11,
  author = {Gilles Benattar and B\'eatrice  B\'erard and Didier Lime and  John Mullins and Olivier H. Roux and Mathieu Sassolas},
  title = {Channel Synthesis for Finite Transducers},
  booktitle = {13th International Conference, on Automata and Formal Languages (AFL'11)},
  month = {August},
  year = {2011},
  address = {Debrecen,  Hungary},
  category = {intc}
}
@inproceedings{thierrymieg-COMPONET-11,
  author = {Y. Thierry-Mieg and B. B\'erard and F. Kordon and D. Lime and O. H. Roux},
  title = {{Compositional Analysis of Discrete Time Petri nets}},
  booktitle = {{1st workshop on Petri Nets Compositions (CompoNet 2011)}},
  year = {2011},
  pages = {17-31},
  address = {Newcastle, UK},
  volume = {726},
  month = {June},
  publisher = {CEUR},
  category = {intc}
}
@inproceedings{traonouez-ATVA-10,
  address = {Singapore},
  author = {Louis-Marie Traonouez and Bartosz Grabiec and Claude Jard and Didier Lime and Olivier H. Roux},
  booktitle = {8th International Symposium on Automated Technology for Verification and Analysis (ATVA 2010)},
  editor = {Ahmed Bouajjani and Wei-Ngan Chin},
  month = sep,
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  title = {{Symbolic Unfolding of Parametric Stopwatch Petri Nets}},
  year = 2010,
  volume = {6252},
  pages = {291--305},
  category = {intc}
}
@inproceedings{grabiec-FORMATS-10,
  address = {Vienna, Austria},
  author = {Bartosz Grabiec and Louis-Marie Traonouez and Claude Jard and Didier Lime and Olivier H. Roux},
  booktitle = {8th International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS 2010)},
  editor = {Krishnendu Chatterjee and Thomas A. Henzinger},
  month = sep,
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  title = {{Diagnosis using Unfoldings  of Parametric Time Petri Nets}},
  year = 2010,
  volume = {6246},
  pages = {137--151},
  category = {intc}
}
@inproceedings{seidner-INCOSE-10,
  author = {Charlotte Seidner and Jean-Philippe Lerat and  Olivier H. Roux},
  title = {Simulation and Verification of Dys]functional Behavior Models: Model Checking for {SE}},
  year = {2010},
  month = jul,
  booktitle = {20{th} International Symposium of the INCOSE},
  address = {Chicago, IL, USA},
  organization = {International Council on Systems Engineering},
  category = {intc}
}
@inproceedings{benattar-formats-09,
  abstract = {  In this paper, we focus on the synthesis of secure timed systems
  which are given by timed automata.
  The security property that the system must satisfy is a
  \emph{non-interference} property. 
  Various notions of non-interference have been defined in the
  literature, and in this paper we focus on \emph{Strong
    Non-deterministic Non-Interference} (SNNI)
  and we study the two following problems: ($1$) check whether it is
  possible to enforce a system to be SNNI; if yes ($2$) compute a
  sub-system which is SNNI.},
  author = {Benattar, Gilles and Cassez, Franck and Lime, Didier and Roux, Olivier H.},
  booktitle = {Proc. of the 7th Int. Conf. on Formal Modeling and Analysis of Timed Systems (FORMATS'09)},
  lex = {B},
  month = sep,
  note = {},
  series = {\begin{rawhtml}Lecture Notes in Computer Science\end{rawhtml}},
  address = {Budapest, Hungary},
  publisher = {Copyright \begin{rawhtml}Springer\end{rawhtml}},
  title = {{Synthesis of Non-Interferent Timed Systems}},
  year = {2009},
  pages = {28-42},
  volume = {5813},
  category = {intc}
}
@inproceedings{boucheneb-ACSD-09,
  author = {Boucheneb, Hanifa  and Rakay, Hind and Roux, Olivier H.},
  title = {Time Arc {Petri} Nets and their analysis},
  booktitle = {9th Int. Conf. on Application of Concurrency to System Design (ACSD'09)},
  year = 2009,
  month = jul,
  address = {Augsburg, Germany},
  category = {intc}
}
@inproceedings{lime-TACAS-09,
  address = {York, United Kingdom},
  author = {Didier Lime and Olivier H. Roux and Charlotte Seidner and Louis-Marie Traonouez},
  editor = {Stefan Kowalewski and Anna Philippou},
  booktitle = {15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2009)},
  month = mar,
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = {5505},
  pages = {54-57},
  title = {Romeo: A Parametric Model-Checker for {Petri} Nets with Stopwatches},
  year = 2009,
  category = {intc}
}
@inproceedings{traonouez-FORMATS-08,
  address = {Saint-Malo, France},
  author = {Louis-Marie Traonouez and Didier Lime and Olivier H. Roux},
  booktitle = {6th International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS 2008)},
  month = sep,
  publisher = {Springer},
  pages = {280-294},
  volume = {5215},
  series = {Lecture Notes in Computer Science},
  pdf = {./fichiers/conf/tlr-formats-2008.pdf},
  title = {Parametric model-checking of time {Petri} nets with stopwatches using the state-class graph},
  year = 2008,
  category = {intc}
}
@inproceedings{magnin-ICATPN-08,
  address = {Xi'an, China},
  author = {Magnin, Morgan and Lime, Didier and Roux, Olivier H.},
  booktitle = {The 29th International Conference on Application and Theory of {Petri} Nets and other models of concurrency (ICATPN 2008)},
  month = jun,
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = {5062},
  pages = {307--326},
  title = {Symbolic state space of Stopwatch {Petri} nets with discrete-time semantics},
  pdf = {./fichiers/conf/mlr-icatpn-2008.pdf},
  year = 2008,
  category = {intc}
}
@inproceedings{bertand-IEEE-08,
  title = { {A} study of the {AADL} mode change protocol},
  author = {{B}ertrand, {D}ominique and {D}{\'e}planche, {A}nne-{M}arie and {F}aucou, {S}{\'e}bastien and {R}oux, {O}livier ({H}.)},
  booktitle = {{P}roceedings of the {IEEE} {I}nternational {C}onference on {E}ngineering {C}omplex {C}omputer {S}ystems - {ICECCS} 2008 3rd {I}nternational {UML} \& {AADL} {W}orkshop },
  publisher = {{IEEE} {C}omputer {S}ociety },
  pages = {288--293 },
  address = {{B}elfast {I}rlande },
  year = {2008},
  category = {intc}
}
@inproceedings{Seidner-CSER-08,
  author = {Seidner, Charlotte and Lerat, Jean-Philippe  and  Roux, Olivier H.},
  title = {Behavior Diagrams Model-Checking: Formal Methods Applied to {S}ystems {E}ngineering and Design},
  year = {2008},
  month = apr,
  booktitle = {6{th} Annual Conference on Systems Engineering Research},
  address = {Los Angeles, CA, USA},
  organization = {University of Southern California},
  category = {intc}
}
@inproceedings{Seidner-ISI-08,
  author = {Seidner, Charlotte and Lerat, Jean-Philippe  and  Roux, Olivier H.},
  title = {Usability and Usefulness of Formal Verification in a System Design Process},
  year = {2008},
  month = jun,
  booktitle = {18{th} International Symposium of the INCOSE},
  address = {Utrecht, Netherlands},
  organization = {International Council on Systems Engineering},
  category = {intc}
}
@inproceedings{cassez-mmm-07,
  author = {Cassez, Franck and Mullins, John and Roux, Olivier H.},
  booktitle = {4th Int. Conf. on Mathematical Methods, Models and Architectures for Computer Network Security (MMM-ACNS'07)},
  month = sep,
  publisher = {Copyright \begin{rawhtml}Springer\end{rawhtml}},
  pages = {159--170},
  series = {Communications in Computer and Inform. Science},
  title = {Synthesis of Non-Interferent Distributed Systems},
  volume = 1,
  abstract = {In this paper, we focus on distributed systems sub ject to 
security issues. Such systems are usually composed of two entities: a 
high level user and a low level user that can both do some actions. The 
security properties we consider are non-interference properties. A system 
is non-interferent if the low level user cannot deduce any information by 
playing its low level actions. Various notions of non-interference have 
been defined in the literature, and in this paper we focus on two of 
them: one trace-based property (SNNI) and another bisimulation-based 
property (BSNNI). 
For these properties we study the problems of synthesis of a high level 
user so that the system is non-interferent. We prove that a most permissive high level user can be computed when one exists. },
  year = {2007},
  pdf = {./fichiers/conf/cmr-mmm-2007.pdf},
  category = {intc}
}
@inproceedings{boyer-ICATPN-07,
  author = {Boyer, Marc and Roux, Olivier H.},
  title = {Comparison of the expressiveness of Arc, Place and Transition Time {Petri} Nets},
  booktitle = {28th International Conference on Application and Theory of Petri Nets and other models of concurrency (ICATPN'07)},
  year = {2007},
  publisher = {Springer-Verlag},
  address = {Siedlce, Poland},
  month = {jun},
  pages = {63-82},
  volume = {4546},
  series = {Lecture Notes in Computer Science},
  note = {(See extended version in {Fundamenta Informaticae})},
  category = {intc}
}
@inproceedings{IS2007,
  author = {Seidner, Charlotte and Lerat, Jean-Philippe  and  Roux, Olivier H.},
  title = {Usability of formal verification on {EFFBD} models: Applying {P}etri nets to {S}ystems {E}ngineering issues},
  booktitle = {17{th} International Symposium of the International Council on Systems Engineering (IS2007)},
  year = {2007},
  address = {San Diego, CA},
  month = {June},
  category = {intc}
}
@inproceedings{gardey-WODES-06,
  author = {Gardey, Guillaume and Roux, Olivier (F.) and Roux, Olivier H.},
  title = {Safety Control Synthesis for Time {Petri} Nets.},
  booktitle = {8th International Workshop on Discrete Event Systems (WODES'06)},
  month = jul,
  year = 2006,
  pages = {222-228},
  publisher = {IEEE Computer Society Press},
  address = {Ann Arbor, USA},
  abstract = {We study some control synthesis problems on an extension of Time
  Petri Nets that model a plant and its environment. The Time Petri
  Net control model both represents controllable and uncontrollable
  events, the problem is then to design a function (\emph{controller})
  such that a given property is fulfilled. We focus our analysis on
  safety properties expressed on the markings of the net and we
  propose a symbolic method to decide the existence of a controller
  that ensures these properties. Unlike existing methods on Time Petri
  Nets, that assume the net is bounded, the method is applicable for
  any Time Petri Nets. A consequence is that it is possible to decide
  the existence of a controller that $k$-bounds the plant. A method is
  then proposed to build a state-based controller and problems raised
  by the implementation (\emph{Zenoness}, \emph{sampling}) of the
  control function on the plant are discussed.},
  pdf = {./fichiers/conf/grr-wodes-2006.pdf},
  category = {intc}
}
@inproceedings{magnin-WODES-06,
  author = {Magnin, Morgan and Molinaro, Pierre and Roux,Olivier H. },
  title = {Decidability, expressivity and state-space computation of Stopwatch {Petri} nets with discrete-time semantics.},
  booktitle = {8th International Workshop on Discrete Event Systems (WODES'06)},
  month = jul,
  pages = {33-38},
  year = 2006,
  publisher = {IEEE Computer Society Press},
  address = {Ann Arbor, USA},
  category = {intc}
}
@inproceedings{berard-FSTTCS-05,
  author = {B\'erard, Beatrice and Cassez, Franck and Haddad, Serge and  Lime, Didier and Roux, Olivier H.},
  title = {When are timed automata weakly timed bisimilar to time {Petri} nets ?},
  booktitle = {25th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2005)},
  month = dec,
  year = 2005,
  volume = {3821},
  pages = {273-284},
  address = {Hyderabad, India},
  series = {Lecture Notes in Computer Science},
  pdf = {./fichiers/conf/bchlr-fsttcs-2005.pdf},
  publisher = {Springer},
  category = {intc}
}
@inproceedings{gardey-SECCO-05,
  author = {Gardey, Guillaume and Mullins, John and Roux, Olivier H.},
  title = {Non-interference control synthesis for security timed automata},
  booktitle = {3rd International Workshop on Security Issues in Concurrency (SecCo'05)},
  year = 2005,
  month = aug,
  series = {Electronic Notes in Theoretical Computer Science},
  publisher = {Elsevier},
  pdf = {./fichiers/conf/gmr-secco-2005.pdf},
  address = {San Francisco, USA},
  category = {intc}
}
@inproceedings{berard-FORMATS-05,
  author = {B\'erard, Beatrice and Cassez, Franck and Haddad, Serge and  Lime, Didier and Roux, Olivier H.},
  title = {Comparison of the expressiveness of Timed Automata and Time {Petri} Nets},
  booktitle = {3rd International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS 05)},
  month = sep,
  year = 2005,
  pages = {211-225},
  volume = {3829},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  address = {Uppsala, Sweden},
  pdf = {./fichiers/conf/bchlr-formats-2005.pdf},
  category = {intc}
}
@inproceedings{berard-ATVA-05,
  author = {B\'erard, Beatrice and Cassez, Franck and Haddad, Serge and  Lime, Didier and Roux, Olivier H.},
  title = {Comparison of Different Semantics for Time {Petri} Nets},
  booktitle = {Automated Technology for Verification and Analysis (ATVA'05)},
  pages = {293-307},
  address = {Taiwan},
  year = 2005,
  pages = {293--307},
  series = {Lecture Notes in Computer Science},
  volume = {3707},
  publisher = {Springer},
  pdf = {./fichiers/conf/bchlr-atva-2005.pdf},
  month = oct,
  category = {intc}
}
@inproceedings{gardey-CAV-05,
  author = {Gardey, Guillaume and Lime, Didier  and Magnin, Morgan  and Roux, Olivier H. },
  title = {Rom\'eo: A Tool for Analyzing time {Petri} nets},
  booktitle = {17th International Conference on Computer Aided Verification
          (CAV'05)},
  month = jul,
  year = 2005,
  pages = {418-423},
  volume = {3576},
  address = {Edinburgh, Scotland, UK},
  series = {Lecture Notes in Computer Science},
  pdf = {./fichiers/conf/glmr-cav-2005.pdf},
  publisher = {Springer},
  category = {intc}
}
@inproceedings{magnin-SOFTMC-05,
  author = {Magnin, Morgan and Lime, Didier   and Roux,Olivier H. },
  title = {An efficient method for computing exact state space of {Petri} nets with stopwatches},
  booktitle = {third International Workshop on Software Model-Checking (SoftMC'05)},
  month = jul,
  volume = {144},
  number = {3},
  pages = {59--77},
  year = 2005,
  address = {Edinburgh, Scotland, UK},
  series = {Electronic Notes in Theoretical Computer Science},
  pdf = {./fichiers/conf/lmr-softmc-2005.pdf},
  publisher = {Elsevier},
  category = {intc}
}
@inproceedings{lime-RTSS-04,
  author = {Lime, Didier and Roux, Olivier H.},
  title = {A translation based method for the timed analysis of scheduling extended time {Petri} nets},
  booktitle = {The 25th IEEE International Real-Time Systems Symposium, (RTSS'04)},
  month = dec,
  year = 2004,
  pages = {187--196},
  address = {Lisbon, Portugal},
  pdf = {./fichiers/conf/lr-rtss-2004.pdf},
  publisher = {IEEE Computer Society Press},
  category = {intc}
}
@inproceedings{cassez-AVOCS-04,
  author = {Cassez, Franck and Roux, Olivier H.},
  title = {Structural Translation from Time {Petri} Nets to Timed Automata},
  booktitle = {Fourth International Workshop on Automated Verification of Critical Systems  (AVoCS'04)},
  pages = {},
  year = 2004,
  month = sep,
  address = {London (UK)},
  series = {Electronic Notes in Theoretical Computer Science},
  note = {(See extended version in Journal of {Systems} and {Software})},
  publisher = {Elsevier},
  category = {intc}
}
@inproceedings{roux-ICATPN-04,
  author = {Roux, Olivier H. and Lime, Didier},
  title = {Time {Petri} Nets with Inhibitor Hyperarcs. {Formal} Semantics and State Space Computation},
  booktitle = {The 25th International Conference on Application and Theory of {Petri} Nets, (ICATPN'04)},
  month = jun,
  year = 2004,
  address = {Bologna, Italy},
  volume = {3099},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  pages = {371--390},
  pdf = {./fichiers/conf/rl-icatpn-2004.pdf},
  note = {Copyright \begin{rawhtml}Springer-Verlag\end{rawhtml}},
  category = {intc}
}
@inproceedings{lime-PNPM-03,
  author = {Lime, Didier and Roux, Olivier H.},
  title = {State class Timed Automaton of a Time {Petri} Net},
  booktitle = {The 10th International Workshop on {Petri} Nets and Performance Models, (PNPM'03)},
  month = sep,
  year = 2003,
  address = {Urbana, USA},
  pages = {124--133},
  publisher = {IEEE Computer Society press},
  note = {(See extended version in Journal of Discrete Event Dynamic Systems)},
  abstract = {In this paper, we propose a method for building the state class graph
of a bounded time Petri net (TPN) as a timed automaton (TA). We consider bounded TPN, whose underlying net
is not necessarily bounded. We prove that the obtained TA
is timed-bisimilar to the initial TPN. The number of clocks of the
automaton is much lower than with other methods available. It allows us to check real-time properties on bounded
TPN with efficient TA model-checkers. We have implemented the method, and give some
experimental results in this paper, illustrating the efficiency of the
algorithm in terms of clock number.},
  category = {intc}
}
@inproceedings{lime-FET-03,
  author = {Lime, Didier and Roux, Olivier H.},
  title = {Expressiveness and analysis of scheduling extended time {Petri} nets},
  booktitle = {5th IFAC International Conference on Fieldbus Systems and their Applications, (FET'03)},
  month = jul,
  year = 2003,
  pages = {193--202},
  address = {Aveiro, Portugal},
  publisher = {Elsevier Science},
  pdf = {./fichiers/conf/lr-fet-2003.pdf},
  note = {Copyright \begin{rawhtml}Elsevier Science\end{rawhtml}},
  abstract = {The most widely used approach for verifying the schedulability of a real-time
system consists of using analytical methods. However, for complex systems with
interdependent tasks and variable execution times, they are not well adapted.
For those systems, an alternative approach is the formal modelisation of
the system and the use
of model-checking, which also allows the verification of more varied scheduling properties.
In this paper, we show how an extension of time Petri nets : scheduling extended time
Petri nets (SETPN), is especially well adapted for the modelisation of
real-time systems and particularly embedded systems and we provide a method
for computing the state space of SETPN. We first propose an exact
computation using a general
polyhedron representation of time constraints, then we propose an
overapproximatiion of the polyhedra to allow the use of much more efficient
data structures, DBMs. We finally describe a particular type of
observers, that
gives us a numeric result (instead of boolean) for the computation of tasks
response times.},
  category = {intc}
}
@inproceedings{gardey-FORMATS-03,
  author = {Gardey, Guillaume and Roux, Olivier H. and Roux, Olivier (F.)},
  title = {A zone-based method for Computing the State Space of a Time {Petri} Net},
  booktitle = {In Formal Modeling and Analysis of Timed Systems, (FORMATS'03)},
  address = {Marseille, France},
  month = sep,
  year = 2003,
  pages = {246--259},
  volume = {2791},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  pdf = {./fichiers/conf/grr-formats-2003.pdf},
  note = {Copyright \begin{rawhtml}Springer-Verlag\end{rawhtml}},
  abstract = {The theory of {\em Petri Nets} provides a general framework to specify the behaviour of real-time
  systems and time extensions have been introduced to take also temporal specifications into
  account. The main method to compute the state space of a Time Petri Net has been introduced by
  \textsc{Berthomieu} and \textsc{Diaz}. It is known as the ``state class
  method''. We present in this paper a new efficient method to compute the state space of a bounded
  Time Petri Net as a marking graph, based on the region graph method used for Timed
  Automaton. Although some limitations induced by Difference Bounded Matrices (DBM)
  have been recently discovered by Bouyer in computing the state space of a Timed
  Automaton (overapproximation), we successfully used DBM in our method.
  The algorithm is proved to be exact with respect to the reachability of a marking and it computes
  a graph which nodes are exactly the reachable markings of the Time Petri Net. The tool implemented
  computes faster than {\em Tina}, a tool for computing the state space using classes, and allows
  to test on-the-fly the reachability of a given marking.},
  category = {intc}
}
@inproceedings{bernot-BIOCONCUR-03,
  author = {Bernot, Gilles and Cassez, Franck and Comet, Jean-Paul  and
Delaplace, Franck and  M\"uller, C\'eline and Roux, Olivier and Roux, Olivier H.},
  title = {Semantics of {Biological Regulatory Networks}},
  booktitle = {Workshop on Concurrent Models in Molecular Biology (BioConcur 2003)},
  year = 2003,
  editor = {Danos, Vincent and Laneve, Cosimo},
  series = {Electronic Notes in Theoretical Computer Science},
  address = {Marseille (France)},
  month = sep,
  pdf = {./fichiers/conf/bccdmrr-bioconcur-2003.pdf},
  publisher = {Elsevier's ENTCS series},
  note = {Copyright \begin{rawhtml}Elsevier\end{rawhtml}},
  category = {intc}
}
@inproceedings{delfieu-WRTP-00,
  author = {Delfieu, David and Molinaro, Pierre and Roux, Olivier H.},
  title = {Analyzing temporal constraints with binary decision diagrams},
  booktitle = {25th IFAC Workshop on Real-Time Programming (WRTP'00)},
  address = {Palma, Spain},
  pages = {131--136},
  year = 2000,
  category = {intc}
}
@inproceedings{roux-ETFA-01,
  title = {Discrete Time approach of Time {Petri} net for real-Time Systems Analysis},
  author = {Roux, Olivier H. and Delfieu, David and Molinaro, Pierre},
  booktitle = {ETFA2001},
  address = {Nice, France},
  month = oct,
  year = 2001,
  publisher = {IEEE Computer Society Press,  Catalog number : 01TH8597 Volume 2},
  pages = {197--204},
  category = {intc}
}
@inproceedings{molinaro-SMC-02,
  title = {Improving the calculus of the marking graph of {Petri} Net with BDD like structure},
  author = {Molinaro, Pierre  and Delfieu, David and Roux, Olivier H.},
  booktitle = {2002 IEEE international conference on systems, man and cybernetics (SMC 02)},
  address = {Hammamet, Tunisia},
  month = oct,
  year = 2002,
  category = {intc}
}
@inproceedings{delfieu-RTS-00,
  title = {Coupling Binary Decision Diagrams with Time {Petri}  Net},
  author = {Delfieu, David and Molinaro, Pierre and Roux, Olivier H.},
  booktitle = {8th international conference on Real-Time and Embedded Systems},
  year = 2000,
  pages = {122--135},
  category = {intc}
}