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{leclercq-QEST-FORMATS-24,
address = {Calgary, Canada},
booktitle = {International Joint Conference on Quantitative Evaluation of
Systems and Formal Modeling and Analysis of Timed Systems
(QEST+FORMATS 2024)},
author = {Loriane Leclercq and Didier Lime and Roux, Olivier H.},
editor = {Jane Hillston and Sadegh Soudjani},
month = sep,
publisher = {Springer},
volume = {14996},
pages = {107--124},
series = {Lecture Notes in Computer Science},
title = {{On Parametric DBMs and their applications to Time Petri Nets}},
year = 2024,
category = {intc}
}
@inproceedings{komenda-WODES-24,
author = {Jan Komenda and S{\'{e}}bastien Lahaye and R\'emi Parrot and Olivier H. Roux},
booktitle = {17th IFAC Workshop on Discrete Event Systems (WODES'24)},
publisher = {IFAC},
month = apr,
address = {Rio de Janeiro, Brazil},
title = {Weakly strong semantics of {Time Petri Nets} for performance evaluations},
year = 2024,
category = {intc}
}
@inproceedings{spriet-FORMATS-23,
author = {Anthony Spriet and Didier Lime and Olivier H. Roux},
booktitle = {21st International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS 2023)},
month = sep,
address = {Antwerp, Belgium},
publisher = {Springer},
volume = {14138},
pages = {122--137},
series = {Lecture Notes in Computer Science},
title = {Timed non-interference under Partial Observability and Bounded Memory},
year = 2023,
category = {intc}
}
@inproceedings{leclercq-ICATPN-23,
author = {Loriane Leclercq and Didier Lime and Olivier H. Roux},
booktitle = {The 44th International Conference on Application and Theory of Petri Nets and Concurrency (Petri Nets 2023)},
month = jun,
address = {Lisbon, Portugal},
publisher = {Springer},
volume = {13929},
series = {Lecture Notes in Computer Science},
title = {{A state class based controller synthesis approach for Time Petri Nets}},
year = 2023,
category = {intc}
}
@inproceedings{haur-ICFEM-22,
author = {Imane Haur and Jean{-}Luc B{\'{e}}chennec and Olivier H. Roux},
booktitle = {23th International Conference on Formal Engineering Methods (ICFEM 2022)},
title = {{Formal verification of the inter-core synchronization of a multi-core RTOS kernel}},
year = 2022,
month = oct,
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {13478},
address = {Madrid, Spain},
category = {intc}
}
@inproceedings{parrot-WODES-22,
author = {R\'emi Parrot and Hanifa Boucheneb and Mika\"el Briday and Olivier H. Roux},
booktitle = {16th IFAC Workshop on Discrete Event Systems (WODES'22)},
publisher = {IFAC},
title = {{Expressiveness and analysis of Timed Petri Nets}},
year = 2022,
month = sep,
address = {Prague, Czechia},
category = {intc}
}
@inproceedings{haur-CODIT-22,
author = {Imane Haur and Jean{-}Luc B{\'{e}}chennec and Olivier H. Roux},
booktitle = {International Conference on Control, Decision and Information Technologies (CODIT 2022)},
title = {{High-level Colored Time Petri Nets for true concurrency modeling in real-time software}},
year = 2022,
month = may,
address = {Istanbul, Turkey},
category = {intc}
}
@inproceedings{parrot-ARITH-21,
author = {R\'emi Parrot and Mika\"el Briday and Olivier H. Roux},
booktitle = {The 28th IEEE International Symposium on Computer Arithmetic (ARITH 2021)},
month = jun,
publisher = {IEEE},
title = {{Pipeline Optimization using a Cost Extension of Timed Petri Nets}},
year = 2021,
category = {intc}
}
@inproceedings{haddad-ICATPN-21,
author = {Serge Haddad and Didier Lime and Olivier H. Roux},
booktitle = {The 42th International Conference on Application and Theory of Petri Nets and Concurrency (Petri Nets 2021)},
month = jun,
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {12734},
title = {{A Turn-Based Approach for Qualitative Time Concurrent Games}},
year = 2021,
category = {intc}
}
@inproceedings{parrot-ICATPN-21,
author = {R\'emi Parrot and Mika\"el Briday and Olivier H. Roux},
booktitle = {The 42th International Conference on Application and Theory of Petri Nets and Concurrency (Petri Nets 2021)},
month = jun,
volume = {12734},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
title = {{Timed Petri Nets with Reset for Pipelined Synchronous Circuit Design}},
year = 2021,
category = {intc}
}
@inproceedings{haur-RTNS-21,
author = {Imane Haur and Jean{-}Luc B{\'{e}}chennec and Olivier H. Roux},
booktitle = {The 29th International Conference on Real-Time Networks and Systems
(RTNS 2021)},
title = {{Formal schedulability analysis based on multi-core RTOS model}},
year = 2021,
category = {intc}
}
@inproceedings{lagha-VALID-20,
author = {Joumana Lagha and Jean{-}Luc B{\'{e}}chennec and S{\'{e}}bastien Faucou and Olivier H. Roux},
booktitle = {The Twelfth International Conference on Advances in System Testing and Validation Lifecycle (VALID 2020)},
month = oct,
address = {Porto, Portugal},
title = {{Toward an Exact Simulation Interval for Multiprocessor Real-Time Systems Validation}},
year = 2020,
isbn = {ISBN: 978-1-61208-830-3},
category = {intc}
}
@inproceedings{lagha-RT-20,
author = {Joumana Lagha and Jean{-}Luc B{\'{e}}chennec and S{\'{e}}bastien Faucou and Olivier H. Roux},
booktitle = {22nd IEEE Real Time Conference (RT2020)},
month = oct,
address = {Virtual},
title = {{Safe Bound on simulation interval for real-time systems for two-phases task model}},
year = 2020,
category = {intc}
}
@inproceedings{lime-ICATPN-19,
author = {Didier Lime and Olivier H. Roux and Charlotte Seidner},
booktitle = {The 40th International Conference on Application and Theory of Petri Nets and Concurrency (Petri Nets 2019)},
volume = {11522},
month = jun,
address = {Germany},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
title = {{Parameter Synthesis for Bounded Cost Reachability in Time Petri Nets}},
year = 2019,
category = {intc}
}
@inproceedings{Bechennec-ACSD-19,
author = { Jean-Luc Bechennec and Didier Lime and Olivier H. Roux},
title = {Control of {DES} with urgency, avoidability and ineluctability},
booktitle = {19th International Conference on Application of Concurrency to System Design (ACSD'19)},
address = {Aachen, Germany},
publisher = {IEEE},
year = 2019,
month = jun,
category = {intc}
}
@inproceedings{emzivat-ITSC-18,
address = {Hawai, USA},
author = {Emzivat, Yrvann and Guzman, Javier Ibanez and Martinet, Philippe and Roux, Olivier H.},
booktitle = {IEEE 21th International Conference on Intelligent Transportation Systems (ITSC 2018)},
title = {A Formal Approach for the Design of a Dependable Perception System for Autonomous Vehicles},
year = 2018,
month = nov,
category = {intc}
}
@inproceedings{boucheneb-ACSD-18,
author = {Hanifa Boucheneb and Didier Lime and Olivier H. Roux and Charlotte Seidner},
title = {Optimal-cost reachability analysis based on time {Petri} nets},
booktitle = {18th International Conference on Application of Concurrency to System Design (ACSD'18)},
year = 2018,
month = jun,
address = {Bratislava, Slovakia},
category = {intc}
}
@inproceedings{chatain-LATA-18,
author = { Chatain, Thomas and Comlan, Maurice and Delfieu, David and Jezequel, Loig and Roux, Olivier H.},
booktitle = {12th International Conference on Language and Automata Theory and Applications (LATA 2018)},
title = {Pomsets and Unfolding of Reset {Petri} Nets},
year = 2018,
month = apr,
volume = {10792},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
category = {intc}
}
@inproceedings{bechennec-CODIT-18,
author = {Bechennec, Jean-Luc and Roux, Olivier H. and Tigori,Toussaint },
booktitle = {International Conference on Control, Decision and Information Technologies (CODIT 2018)},
title = {Formal model-based conformance verification of an {OSEK/VDX} compliant {RTOS}},
year = 2018,
month = apr,
category = {intc}
}
@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,
month = oct,
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,
volume = {10419},
publisher = {Springer},
pages = {58-73},
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 = jun,
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 = {Jun},
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}
}