article.bib
@comment{{This file has been generated by bib2bib 1.96}}
@comment{{Command line: ./bib2bib -oc selection -ob article.bib -c 'category : "intJournal"' mesPublications.bib}}
@article{haur-CS-23,
author = {Imane Haur and Jean-Luc B{\'{e}}chennec and Olivier H. Roux},
title = {Model-Checking of Concurrent Real-Time Software Using {High-Level Colored Time Petri Nets} with Stopwatches},
journal = {Cybernetics and Systems},
pages = {1-31},
year = {2023},
month = sep,
publisher = {Taylor & Francis},
note = {Taylor & Francis},
doi = {10.1080/01969722.2023.2247261},
url = {https://doi.org/10.1080/01969722.2023.2247261},
category = {intJournal}
}
@article{haur-SQJ-23,
author = {Imane Haur and Jean{-}Luc B{\'{e}}chennec and Olivier H. Roux},
journal = {Software Quality Journal},
title = {{ Formal verification process of the compliance of a multicore AUTOSAR OS}},
year = 2023,
volume = {31},
number = {2},
pages = {497--531},
month = jun,
publisher = {Springer},
doi = {10.1007/s11219-023-09626-4},
note = {Springer},
category = {intJournal}
}
@article{parrot-DEDS-23,
author = {R\'emi Parrot and Mika\"el Briday and Olivier H. Roux},
title = {Design and verification of pipelined circuits with Timed Petri Nets},
journal = {Discrete Event Dynamic Systems - Theory and Applications (DEDS)},
publisher = {Springer},
note = {Springer},
volume = {33},
number = {1},
year = {2022},
pages = {1--24},
month = dec,
doi = {10.1007/s10626-022-00371-7},
category = {intJournal}
}
@article{bernabeu-DEDS-23,
author = {Antoine Bernabeu and Jean-Luc B\'echennec and Mika\"el Briday and S\'ebastien Faucou and Olivier H. Roux},
title = {Cost-optimal timed trace synthesis for scheduling of intermittent embedded systems},
journal = {Discrete Event Dynamic Systems - Theory and Applications (DEDS)},
publisher = {Springer},
note = {Springer},
doi = {10.1007/s10626-022-00372-6},
volume = {33},
number = {1},
year = {2022},
pages = {63--93},
month = dec,
category = {intJournal}
}
@article{andre-LMCS-22,
author = {{\'{E}}tienne Andr{\'{e}} and
Didier Lime and
Olivier H. Roux},
title = {Reachability and liveness in parametric timed automata},
journal = {Logical Methods in Computer Science},
volume = {18},
number = {1},
year = {2022},
pages = {1--31},
month = feb,
pdf = {https://arxiv.org/pdf/2004.09171.pdf},
category = {intJournal}
}
@article{jovanovic-IEEETAC-22,
author = {Jovanovi\'c, Aleksandra and Lime, Didier and Roux, Olivier H.},
title = {{Control of Real-time Systems with Integer Parameters}},
journal = {IEEE Transactions on Automatic Control},
publisher = {IEEE},
year = {2022},
volume = {67},
number = {1},
pages = {75--88},
month = jan,
doi = {10.1109/TAC.2020.3046578},
category = {intJournal}
}
@article{lime-FI-21,
author = {Didier Lime and Olivier H. Roux and Charlotte Seidner},
title = {Cost Problems for Parametric Time Petri Nets},
journal = {Fundamenta Informaticae},
volume = {183},
number = {1-2},
publisher = {IOS Press},
pages = {97--123},
doi = {10.3233/FI-2021-2083},
year = 2021,
pdf = {https://arxiv.org/pdf/2109.03658.pdf},
category = {intJournal}
}
@article{bechennec-DEDS-21,
author = { Jean-Luc Bechennec and Didier Lime and Olivier H. Roux},
journal = {Discrete Event Dynamic Systems - Theory and Applications (DEDS)},
title = {{Logical Time Control of concurrent DES}},
publisher = {Springer},
volume = {31},
number = {2},
pages = {185--217},
note = {Springer},
doi = {10.1007/s10626-020-00333-x},
year = 2021,
category = {intJournal}
}
@article{chatain-IC-20,
author = { Chatain, Thomas and Comlan, Maurice and Delfieu, David and Jezequel, Loig and Roux, Olivier H.},
title = {{Pomset Bisimulation and Unfolding for Reset Petri Nets}},
journal = {Information and Computation},
volume = {283},
pages = {104674},
year = {2020},
issn = {0890-5401},
doi = {https://doi.org/10.1016/j.ic.2020.104674},
publisher = {Elsevier},
note = {issn 0890-5401, Elsevier},
category = {intJournal}
}
@article{jovanovic-IJC-19,
author = {Jovanovi\'c, Aleksandra and Lime, Didier and Roux, Olivier H.},
title = {{A Game Approach to the Parametric Control of Real-time Systems}},
journal = {International Journal of Control},
publisher = {Taylor \& Francis},
volume = {92},
number = {9},
pages = {2025--2036},
year = 2019,
note = {Taylor and Francis },
doi = {10.1080/00207179.2018.1426883},
category = {intJournal}
}
@article{bechennec-IEEEDT-18,
journal = {IEEE Design \& Test},
title = {{Testing Real Time Systems with runtime enforcement}},
publisher = {IEEE},
author = {B{\'e}chennec, Jean{-}Luc and Brun, Matthias and Faucou, S{\'e}bastien and Givel, Louis{-}Marie and Roux, Olivier H.},
year = {2018},
volume = {35},
number = {4},
pages = {31--37},
note = {IEEE},
month = aug,
doi = {10.1109/MDAT.2018.2791801},
issn = {2168-2364},
category = {intJournal}
}
@article{tigori-TECS-17,
year = 2017,
journal = {ACM Transactions on Embedded Computing Systems},
title = {Formal model-based synthesis of application specific static {RTOS}},
publisher = {ACM},
author = {Tigori, Toussaint and B{\'e}chennec, Jean-Luc and Faucou, S{\'e}bastien and Roux, Olivier H.},
issue_date = {September 2017},
volume = {16},
number = {4},
month = may,
year = {2017},
issn = {1539-9087},
pages = {97:1--97:25},
articleno = {97},
numpages = {25},
doi = {10.1145/3015777},
acmid = {3015777},
publisher = {ACM},
category = {intJournal}
}
@article{beldiceanu-computing-17,
title = {{Towards energy-proportional Clouds partially powered by renewable energy}},
author = {Beldiceanu, Nicolas and Dumas Feris, B{\'a}rbara and Gravey, Philippe and Hasan, Sabbir and Jard, Claude and Ledoux, Thomas and Li, Yunbo and Lime, Didier and Madi-Wamba, Gilles and Menaud, Jean-Marc and Morel, Pascal and Morvan, Michel and Moulinard, Marie-Laure and Orgerie, Anne-C{\'e}cile and Pazat, Jean-Louis and Roux, Olivier H. and Sharaiha, Ammar},
journal = {{Computing}},
publisher = {{Springer Verlag}},
volume = {99},
number = {1},
month = jan,
year = {2017},
doi = {https://doi.org/10.1007/s00607-016-0503-z},
category = {intJournal}
}
@article{girault-DEDS-16,
year = 2016,
issn = {0924-6703},
journal = {Discrete Event Dynamic Systems - Theory and Applications (DEDS)},
doi = {10.1007/s10626-015-0222-1},
title = {On-line compositional controller synthesis for {AGV}},
publisher = {Springer},
note = {Springer},
volume = {26},
number = {4},
pages = {583-610},
author = {Girault, Johan and Loiseau, Jean-Jacques and Roux, Olivier H.},
pdf = {./fichiers/glr-deds-2016.pdf},
category = {intJournal}
}
@article{jovanovic-IEEETSE-15,
author = {Jovanovi\'c, Aleksandra and Lime, Didier and Roux, Olivier H.},
title = {{Integer Parameter Synthesis for Real-Time Systems}},
journal = {IEEE Transactions on Software Engineering (TSE)},
publisher = {IEEE},
volume = {41},
number = {5},
pages = {445-461},
year = 2015,
doi = {10.1109/TSE.2014.2357445},
pdf = {./fichiers/jlr-IEEETSE-2015.pdf},
category = {intJournal}
}
@article{benattar-IJC-15,
author = {Benattar, Gilles and Cassez, Franck and Lime, Didier and Roux, Olivier H.},
title = {{Control and Synthesis of Non-Interferent Timed Systems}},
journal = {International Journal of Control},
publisher = {Taylor and Francis},
volume = {88},
number = {2},
pages = {217-236},
year = 2015,
http = {http://www.tandfonline.com/doi/abs/10.1080/00207179.2014.944356#.U9OCdhaWXc8},
note = {Taylor and Francis},
pdf = {./fichiers/bclr-ijc-2015.pdf},
category = {intJournal}
}
@article{jard-FI-14,
author = {Jard, Claude and Lime, Didier and Roux, Olivier H.},
title = {{Blending Timed Formal Models with Clock Transition Systems}},
journal = {Fundamenta Informaticae},
publisher = {IOS Press},
year = 2014,
volume = {129},
number = {1-2},
pages = {85-100},
pdf = {./fichiers/jlr-fi-2014.pdf},
category = {intJournal}
}
@article{lelionnais-IJASM-14,
title = {Formal Synthesis of Real-Time System Models in a {MDE} Approach},
author = {Lelionnais, C\'edrick and Brun, Matthias and Delatour, J\'er\^ome and Roux, Olivier H. and Seidner, Charlotte },
journal = {International Journal on Advances in Systems and Measurement},
year = 2014,
volume = {7},
number = {1-2},
publisher = {IARA},
http = {http://www.iariajournals.org/systems_and_measurements/},
category = {intJournal}
}
@article{jard-FMSD-13,
author = {Jard, Claude and Lime, Didier and Roux, Olivier H. and Traonouez, Louis-Marie },
journal = {Formal Methods in System Design (FMSD)},
publisher = {Springer},
title = {Symbolic Unfolding of Parametric Stopwatch {Petri} Nets},
year = 2013,
volume = {43},
number = {3},
pages = {493-519},
pdf = {./fichiers/jlrt-fmsd-2013.pdf},
note = {Springer},
category = {intJournal}
}
@article{lime-DEDS-13,
author = {Lime, Didier and Martinez, Claude and Roux, Olivier H.},
journal = {Journal of Discrete Event Dynamic Systems - Theory and Applications (DEDS)},
publisher = {Springer},
title = {Shrinking of Time {Petri} nets},
year = 2013,
volume = {23},
number = {4},
pages = {419-438},
pdf = {./fichiers/lmr-deds-2013.pdf},
note = {Springer},
category = {intJournal}
}
@article{berard-TCS-13,
journal = {Theoretical Computer Science (TCS)},
title = {The Expressive Power of Time {Petri} Nets},
author = {B\'eatrice B\'erard and Franck Cassez and Serge Haddad and Didier Lime and Olivier H. Roux},
year = {2013},
volume = {474},
pages = {1-20},
publisher = {Elsevier},
pdf = {./fichiers/bchlr-tcs-2013.pdf},
http = {http://www.sciencedirect.com/science/article/pii/S0304397512010845},
note = {Elsevier},
category = {intJournal}
}
@article{bennatar-IJFCS-12,
author = {Benattar, Gilles and B\'erard, B\'eatrice and Lime, Didier and Mullins, John and Roux, Olivier H. and Sassolas, Mathieu},
title = {Channel Synthesis for Finite Transducers},
journal = {International Journal of Foundations of Computer Science},
volume = {23},
number = {6},
pages = {1241-1260},
year = 2012,
publisher = {World Scientific Publishing Company},
pdf = {./fichiers/bblmrs-jfc-2012.pdf},
http = {http://www.worldscientific.com/doi/abs/10.1142/S0129054112400503},
category = {intJournal}
}
@article{boucheneb-JLC-09,
author = {Boucheneb, Hanifa and Gardey, Guillaume and Roux, Olivier H.},
title = {{TCTL} model checking of Time {Petri} Nets},
journal = {Journal of Logic and Computation},
publisher = {Oxford University Press,},
year = 2009,
month = dec,
volume = {19},
number = {6},
pages = {1509-1540},
abstract = {In this paper, we consider \emph{subscript} TCTL for Time Petri Nets
(TPN-TCTL) for which temporal operators are extended with a time
interval, specifying a time constraint on the firing sequences.
We prove that the model-checking of a TPN-TCTL formula on a bounded TPN is decidable and is a
PSPACE-complete problem.
We propose a zone based state space abstraction that preserves
marking reachability and traces of the TPN. As for Timed
Automata (TA), the abstraction may use an over-approximation
operator on zones to enforce the termination. A coarser (and
efficient) abstraction is then provided and proved exact w.r.t.
marking reachability and traces (LTL properties).
Finally, we consider a subset of TPN-TCTL properties for
which it is possible to propose efficient on-the-fly model-checking
algorithms. Our approach consists in computing and exploring the
zone based state space abstraction.},
note = {Copyright \begin{rawhtml}Oxford Press\end{rawhtml}},
http = {http://logcom.oxfordjournals.org/cgi/content/abstract/19/6/1509},
pdf = {./fichiers/bgr-jlc-2009.pdf},
category = {intJournal}
}
@article{Traonouez-JUCS-09,
author = {Louis-Marie Traonouez and Didier Lime and Olivier H. Roux},
journal = {Journal of Universal Computer Science, A publication of Graz University of Technology and Universiti Malaysia Sarawak},
title = {Parametric Model-Checking of Stopwatch {Petri} Nets},
abstract = {At the border between control and verification, parametric verification can be used to synthesize constraints on the parameters to ensure that a system verifies given specifications. In this paper we propose a new framework for the parametric verification of time Petri nets with stopwatches. We first introduce a parametric extension of time Petri nets with inhibitor arcs (ITPNs) with temporal parameters and we define a symbolic representation of the parametric state-space based on the classical state-class graph method. Then, we propose semi-algorithms for the parametric modelchecking of a subset of parametric TCTL formulae on ITPNs. These results have been implemented in the tool Romeo and we illustrate them in a case-study based on a scheduling problem.},
year = {2009},
volume = {15},
number = {17},
pages = {3273--3304},
month = dec,
http = {http://www.jucs.org/jucs_15_17/parametric_model_checking_of},
pdf = {./fichiers/tlr-jucs-2009.pdf},
category = {intJournal}
}
@article{magnin-FI-09a,
author = {Magnin, Morgan and Molinaro, Pierre and Roux,Olivier H. },
journal = {Fundamenta Informaticae},
title = {Expressiveness of {Petri} Nets with Stopwatches. {Dense-time} part.},
year = 2009,
volume = {97},
number = {1-2},
pages = {111-138},
http = {http://www.mimuw.edu.pl/~fundam/FI/previous/vol97},
category = {intJournal}
}
@article{magnin-FI-09b,
author = {Magnin, Morgan and Molinaro, Pierre and Roux,Olivier H. },
journal = {Fundamenta Informaticae},
title = {Expressiveness of {Petri} Nets with Stopwatches. {Discrete-time} part.},
year = 2009,
volume = {97},
number = {1-2},
pages = {139-176},
http = {http://www.mimuw.edu.pl/~fundam/FI/previous/vol97},
category = {intJournal}
}
@article{lime-JRTS-09,
author = {Lime, Didier and Roux, Olivier H.},
title = {Formal verification of real-time systems with preemptive scheduling},
journal = {Journal of Real-Time Systems},
volume = {41},
number = {2},
year = 2009,
pages = {118-151},
publisher = {Springer},
note = {Copyright \begin{rawhtml}Springer\end{rawhtml}},
year = 2009,
pdf = {./fichiers/lr-jrts-2009.pdf},
http = {http://www.springerlink.com/content/m40671u08r672215/},
abstract = {In this paper, we propose a method for the verification of timed properties
for real-time systems featuring a preemptive scheduling policy: the system,
modeled as a scheduling time Petri net, is first translated into a linear hybrid
automaton to which it is time-bisimilar. Timed properties can then be verified
using \hytech. The efficiency of this approach leans on two major points:
first, the translation features a minimization of the number of variables (clocks) of
the resulting automaton, which is a critical parameter for the efficiency of
the ensuing verification. Second, the translation is performed by an
over-approximating algorithm, which is based on Difference Bound Matrix and
therefore efficient, that nonetheless produces a time-bisimilar automaton
despite the over-approximation. The
proposed modeling and verification method are generic enough to account for
many scheduling policies. In this paper, we specifically show how to deal
with Fixed Priority and Earliest Deadline First policies, with the possibility
of using Round-Robin
for tasks with the same priority. We have implemented the method and give
some experimental results illustrating its efficiency.},
category = {intJournal}
}
@article{Seidner-IEEE-08,
author = {Seidner, Charlotte and Roux, Olivier H.},
title = {Formal {M}ethods for {S}ystems {E}ngineering {B}ehavior Models},
year = {2008},
journal = {IEEE Transactions on Industrial Informatics. Special Issue on Formal Methods for Embedded Systems Design},
publisher = {IEEE Computer Society Press},
volume = {4},
number = {4},
pages = {280-291},
note = {IEEE Computer Society Press},
abstract = {Safety analysis in Systems Engineering (SE) processes, as usually implemented, rarely relies on formal methods such as model checking since such techniques, however powerful and mature, are deemed too complex for efficient use.
This paper thus aims at improving the verification practice in SE design: considering the widely-used model of EFFBDs (Enhanced Function Flow Block Diagrams), it formally establishes its syntax and behavioral semantics.
It also proposes a structural translation of EFFBDs to transition time Petri nets (TPNs); this translation is then proved to preserve the behavioral semantics (i.e. timed bisimilarity).
After proving results on the boundedness of the resulting TPNs, it was possible to extend a number of fundamental properties (such as the decidability of liveness, state-access, etc.) from bounded TPNs to so-called \emph{bounded EFFBDs}.
Finally, these results led to implement and integrate an operational formal verification tool within a development platform, used in systems design for defense applications, where the underlying complexity is totally concealed from the end-user. },
pdf = {./fichiers/sr-ieeetii-2008.pdf},
category = {intJournal}
}
@article{boyer-FI-08,
author = {Boyer, Marc and Roux, Olivier H.},
journal = {Fundamenta Informaticae},
title = {On the compared expressiveness of arc, place and transition time {Petri} Nets},
volume = {88},
number = {3},
year = 2008,
pages = {225-249},
abstract = {In this paper, we consider safe Time Petri Nets where time intervals (strict and large) are associated with places (TPPN), arcs (TAPN) or transitions (TTPN).
We give the formal strong and weak semantics of these models in terms of Timed Transition Systems.
We compare the expressiveness of the six models w.r.t. (weak) timed bisimilarity (behavioral semantics).
The main results of the paper are : (i)~with strong semantics, TAPN is strictly more expressive than TPPN and TTPN~; (ii)~with strong semantics TPPN and TTPN are incomparable~; (iii)~TTPN with strong semantics and TTPN with weak semantics are incomparable.
Moreover, we give a complete classification by a set of 9 relations explained in a figure.},
note = {Copyright \begin{rawhtml}IOS Press\end{rawhtml}},
pdf = {./fichiers/br-fi-2008.pdf},
http = {http://fi.mimuw.edu.pl/},
category = {intJournal}
}
@article{berard-TCS-08,
author = {B\'erard, B\'eatrice and Cassez, Franck and Haddad, Serge and Didier Lime and Roux, Olivier H.},
journal = {Theoretical Computer Science},
publisher = {Elsevier},
title = {When are timed automata weakly timed bisimilar to time {Petri} nets?},
pages = {202-220},
volume = {403},
number = {2-3},
year = 2008,
pdf = {./fichiers/bchlr-tcs-2008.pdf},
note = {Copyright \begin{rawhtml}Elsevier\end{rawhtml}},
category = {intJournal}
}
@article{berthomieu-DEDS-07,
author = {Berthomieu, Bernard and Lime, Didier and Roux, Olivier H. and Vernadat, Francois},
journal = {Journal of Discrete Event Dynamic Systems - Theory and Applications (DEDS)},
publisher = {Springer},
title = {Reachability Problems and Abstract State Spaces for Time {Petri}
Nets with Stopwatches},
pages = {133-158},
volume = {17},
number = {2},
year = 2007,
pdf = {./fichiers/blrv-deds-2007.pdf},
note = {Copyright \begin{rawhtml}Springer\end{rawhtml}},
abstract = {Several extensions of Time Petri nets (TPNs) have been proposed for modeling suspension and resumption of actions in timed systems. We first introduce a simple class of TPNs extended with stopwatches (SwTPNs), and present a semi-algorithm for building exact representations of the behavior of SwTPNs. Then, we prove that state reachability in SwTPNs and all similar models is undecidable, even when bounded, which solves an open problem. Finally, we discuss overapproximation methods yielding finite abstractions of their behavior for a subclass of bounded SwTPNs, and propose a new one based on a quantization of the polyhedra representing temporal information. By, adjusting a parameter, the exact behavior can be approximated as closely as desired.},
category = {intJournal}
}
@article{cassez-JSS-06,
author = {Cassez, Franck and Roux, Olivier H.},
title = {Structural Translation from {Time Petri Nets to Timed Automata} -- {Model-Checking Time Petri Nets via Timed Automata}},
pages = {1456-1468},
volume = {79},
number = {10},
year = 2006,
publisher = {Elsevier},
journal = {The journal of Systems and Software},
pdf = {./fichiers/cr-jss-2006.pdf},
note = {Copyright \begin{rawhtml}Elsevier\end{rawhtml}},
category = {intJournal}
}
@article{lime-DEDS-06,
author = {Lime, Didier and Roux, Olivier H.},
title = {Model checking of time {Petri} nets using the state class
timed automaton},
journal = {Journal of Discrete Events Dynamic Systems - Theory and Applications (DEDS)},
pages = {179--205},
volume = {16},
number = {2},
year = 2006,
pdf = {./fichiers/lr-deds-2006.pdf},
note = {Copyright \begin{rawhtml}Springer-Kluwer\end{rawhtml}},
publisher = {Kluwer Academic Publishers},
category = {intJournal}
}
@article{gardey-TPLP-06,
author = {Gardey, Guillaume and Roux, Olivier H. and Roux, Olivier (F.)},
title = {State Space Computation and Analysis of Time {Petri} Nets},
journal = {Theory and Practice of Logic Programming (TPLP). Special Issue on Specification
Analysis and Verification of Reactive Systems},
year = 2006,
pages = {301--320},
volume = {6},
number = {3},
publisher = {Cambridge University Press},
abstract = {We present in this paper a forward zone-based algorithm to compute the state space
of a bounded Time Petri Net: the method is different and more efficient than the classical State
Class Graph. We prove the algorithm to be exact with respect to the reachability problem.
Furthermore, we propose a translation of the computed state space into a Timed Automaton, proved
to be timed bisimilar to the original Time Petri Net. },
pdf = {./fichiers/grr-tplp-2006.pdf},
note = {Copyright \begin{rawhtml}Cambridge Press\end{rawhtml}},
category = {intJournal}
}
@article{roux-JESA-02,
author = {Roux, Olivier H. and D\'eplanche, Anne-Marie},
title = {A T-time {Petri} net extension for real time-task scheduling
modeling},
journal = {European Journal of Automation (JESA)},
volume = {36},
number = {7},
year = 2002,
pages = {973--987},
publisher = {Hermes Science},
pdf = {./fichiers/rd-jesa-2002.pdf},
isbn = {ISBN 2-7462-0573-4},
note = {Copyright \begin{rawhtml}Hermes-Science\end{rawhtml}},
abstract = {In order to analyze whether timing requirements of a real-time application are met,
we propose an extension of the T-time {Petri} net model which takes into account the scheduling
of the software tasks distributed over a multi-processor hardware architecture.
The paper is concerned with static priority pre-emptive based scheduling.
This extension consists in mapping into the {Petri} net model the way the different schedulers
of the system activate or suspend the tasks. This relies on the introduction of two new attributes
for the places (allocation and priority). First we give the formal semantics of this extended model
as a timed transition system (TTS). Then we propose a method for its analysis consisting in the
computation of the state class graph. Thus the verification of timing properties can be conducted
(possibly together with an observator) and comes to analyze the such obtained state class graph.},
category = {intJournal}
}
@article{roux-JESA-96,
author = {Roux, Olivier H. and Molinaro, Pierre},
title = {Deadlock detection and processing in {Oreste}},
journal = {European Journal of Automation (RAIRO - APII - JESA)},
volume = {30},
number = {4},
pages = {519--542},
year = 1996,
isbn = {ISSN 0296-1598},
publisher = {Hermes Science},
category = {intJournal}
}