Séminaires

Le prochain

07/06/2024
22/03/2024
12/01/2024

10/11/2023
15/09/2023

11/06/2021

20/12/2019
11/10/2019
24/05/2019
22/03/2019
25/01/2019

Séminaires 2018
Séminaires 2017
Séminaires 2016
Séminaires 2015
Séminaires 2014
Séminaires 2013
Séminaires 2012
Séminaires 2011
Séminaires 2010
Séminaires 2009
Séminaires 2008
Séminaires 2007
Séminaires 2006
Séminaires 2005


mod. 09-09-2024

Publications en commun

Introduction

Cette page référence les publications dans le cadre des activités de MeFoSyLoMa. Nous ne listons que les publications impliquant au moins deux équipes du groupe.

2021

  1. B. Bérard, S. Haddad, C. Picaronny, M. Safey El Din, M. Sassolas : "Polynomial interrupt timed automata: Verification and expressiveness", Information and Computation, vol.277, (Elsevier) (2021) [DOI]

2020

  1. B. Bérard, B. Bollig, P. Bouyer, M. Függer, N. Sznajder : "Synthesis in Presence of Dynamic Links", Proceedings of the 11th International Symposium on Games, Automata, Logics, and Formal Verification (GandALF'20), Brussels (on line), Belgium (2020) [DOI]
  2. N. Sznajder, B. Bérard, B. Bollig, M. Lehaut : "Parameterized Synthesis for Fragments of First-Order Logic over Data Words", Proceedings of the 23rd International Conference on Foundations of Software Science and Computation Structures (FoSSaCS'20), vol. 12077, Lecture Notes in Computer Science, Dublin, Ireland, pp. 97-118, (Springer) (2020) [DOI]
  3. Patricia Bouyer, Stéphane Le Roux, Youssouf Oualhadj, Mickael Randour, Pierre Vandenhove: Games Where You Can Play Optimally with Arena-Independent Finite Memory. CONCUR2020: 24:1-24:22

2019

  1. Étienne André, Emmanuel Coquard, Laurent Fribourg, Jawher Jerray, and David Lesens. Scheduling synthesis for a launcher flight control using parametric stopwatch automata. In Jörg Keller and Wojciech Penczek, editors, ACSD. IEEE, 2019. To appear. [ bib ]
  2. Étienne André, Laurent Fribourg, Jean-Marc Mota, and Romain Soulat. Verification of an industrial asynchronous leader election algorithm using abstractions and parametric model checking. In Constantin Enea and Ruzica Piskac, editors, VMCAI, LNCS, pages 409--424. Springer, 2019. [ bib | DOI ]

2018

  1. H. Metin, S. Baarir, M. Colange, and F. Kordon. CDCLSym : Introducing Effective Symmetry Breaking in SAT Solving. 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), volume10877 Of LNCS, pages 99-114, Springer, April 2018 - get pdf - url to publisher
  2. F. Belardinelli, I. Boureanu, C. Dima, V. Malvone; Verifying Strategic Abilities in Multi-agent Systems with Private Data-Sharing (extended abstract). AAMAS 2019: 1820-1822.
  3. F. Belardinelli, C. Dima, A. Murano: Bisimulations for Logics of Strategies: A Study in Expressiveness and Verification. Proc. of the 16th International Conference on Principles of Knowledge Representation and Reasoning (KR2018), Tempe, 425-434
  4. Béatrice Bérard, Patricia Bouyer, and Vincent Jugé. Finite bisimulations for dynamical systems with overlapping trajectories. In Ghica and Jung, pages 26:1--26:17. [ bib | DOI | http ]
  5. Béatrice Bérard, Stefan Haar, and Loïc Hélouët. Hyper partial order logic. In Ganguly and Pandya , pages 20:1--20:21. [ bib | DOI | http ]
  6. Benoît Barbot, Béatrice Bérard, Yann Duplouy, and Serge Haddad. Integrating simulink models into the model checker cosmos. In Khomenko and Roux , pages 363--373. [  DOI | http ]
  7. Béatrice Bérard, Olga Kouchnarenko, John Mullins, and Mathieu Sassolas. Opacity for linear constraint markov chains. Discrete Event Dynamic Systems, 28(1):83--108, 2018. [  DOI | http ]
  8. Béatrice Bérard, Stefan Haar, Sylvain Schmitz, and Stefan Schwoon. The complexity of diagnosability and opacity verification for petri nets. Fundam. Inform., 161(4):317--349, 2018. [ bib | DOI | http ]

2017

  1. B. Bérard, S. Haddad, and E. Lefaucheux. Probabilistic Disclosure: Maximisation vs. Minimisation. In Proceedings of the 37th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'17), volume 93 of Leibniz International Proceedings in Informatics, pages 13:1--13:14, Kanpur, India, December 2017. Leibniz-Zentrum für Informatik. doi: 10.4230/LIPIcs.FSTTCS.2017.13.
  2. S. Haar, S. Haddad, T. Melliti, and S. Schwoon. Optimal constructions for active diagnosis. Journal of Computer and System Sciences, 83(1):101--120, 2017. doi: 10.1016/j.jcss.2016.04.007.
  3. L. Le Frioux, S. Baarir, J. Sopena, and F. Kordon. PaInleSS: a Framework for Parallel SAT Solving. 20th International Conference on Theory and Applications of Satisfiability Testing (SAT) volume 10491 of LNCS, pages 233-250, Springer, August 2017 - get pdf - url to publisher
  4. F. Belardinelli, R. Condurache, C. Dima, W. Jamroga, A. V. Jones; Bisimulations for Verifying Strategic Abilities with an Application to ThreeBallot. Proc. of the 16th International Conference on Autonomous Agents and Multiagent Systems (AAMAS17), Sao Paulo, 2017.
  5. Benoît Barbot, Béatrice Bérard, Yann Duplouy, and Serge Haddad. Statistical model-checking for autonomous vehicle safety validation. In SIA Simulation Numérique, 2017. [ http ]
  6. Béatrice Bérard, Stefan Haar, Sylvain Schmitz, and Stefan Schwoon. The complexity of diagnosability and opacity verification for petri nets. In Wil M. P. van der Aalst and Eike Best, editors, Application and Theory of Petri Nets and Concurrency - 38th International Conference, PETRI NETS 2017, Zaragoza, Spain, June 25-30, 2017, Proceedings, volume 10258 of Lecture Notes in Computer Science, pages 200-220. Springer, 2017. [ DOI ]
  7. Béatrice Bérard, Serge Haddad, and Engel Lefaucheux. Probabilistic disclosure: Maximisation vs. minimisation. In FSTTCS 2017, 2017.
  8. Stefan Haar, Serge Haddad, Tarek Melliti, and Stefan Schwoon. Optimal constructions for active diagnosis. Journal of Computer and System Sciences, 83(1):101-120, 2017.
  9. Ludovic Le Frioux, Souheib Baarir, Julien Sopena, and Fabrice Kordon. PaInleSS: A Framework for Parallel SAT Solving, pages 233-250. Springer International Publishing, Cham, 2017. [ DOI | http ]
  10. E. Renault, A. Duret-Lutz, F. Kordon, and D. Poitrenaud. Variations on parallel explicit emptiness checks for generalized büchi automata. International Journal on Software Tools for Technology Transfer, 19(6):653-673, Nov 2017. [ DOI | http ]

2016

  1. Étienne André, Thomas Chatain and César Rodríguez. Preserving Partial Order Runs in Parametric Time Petri Nets. Transactions on Embedded Computing Systems 16(2), pages 43:1–43:26, December 2016.
  2. B. Bérard, S. Haddad, A. Jovanovi? and D. Lime. Interrupt Timed Automata with Auxiliary Clocks and Parameters. Fundamenta Informaticae 143(3-4), pages 235-259, 2016.
  3. F. Kordon, H. Garavel, L. Hillah, E. Paviot-Adet, L. Jezequel, C. Rodrìguez, and F. Hulin-Hubard. MCC’2015 - the fifth model checking contest. T. Petri Nets and Other Models of Concurrency, 11:262– 273, 2016.
  4. A. Duret-Lutz, F. Kordon, D. Poitrenaud, and E. Renault. Heuristics for checking liveness properties with partial order reductions. In C. Artho, A. Legay, and D. Peled, editors, Automated Technology for Verification and Analysis - 14th International Symposium, ATVA 2016, Chiba, Japan, October 17-20, 2016, Proceedings, volume 9938 of Lecture Notes in Computer Science, pages 340–356, 2016.

2015

  1. B. Bérard, J. Mullins, and M. Sassolas. Quantifying Opacity. Mathematical Structures in Computer Science, 25(2):361–403, 2015
  2. E. Renault A. Duret-Lutz and F. Kordon and D. poitrenaud. Parallel Explicit Model Checking for Generalized Buchi Automata. 21th International Conference on Tools and Algorithms for the Construction and Analysis of Systems - TACAS, Springer, April 2015
  3. P. Ballarini, B. Barbot, M. Duflot, S. Haddad and N. Pekergin. HASL: A New Approach for Performance Evaluation and Model Checking from Concepts to Experimentation. Performance Evaluation, 2015.
  4. A. Methni, M. Lemerre, B. Ben Hedia, S. Haddad and K. Barkaoui. Specifying and Verifying Concurrent C Programs with TLA+. In Formal Techniques for Safety-Critical Systems, Communications in Computer and Information Science 476, pages 206-222. Springer, 2015
  5. É. André, T. Chatain and C. Rodríguez. Preserving Partial Order Runs in Parametric Time Petri Nets. In Stefan Haar and Roland Meyer (eds.), ACSD’15, IEEE, June 2015
  6. É. André and N. Markey. Language Preservation Problems in Parametric Timed Automata. In Sriram Sankaranarayanan and Enrico Vicario (eds.), FORMATS’15, Springer LNCS, September 2015
  7. B. B´erard, S. Haddad, C. Picaronny, M. Safey El Din, and M. Sassolas. Polynomial interrupt timed au- tomata. In M. Bojanczyk, S. Lasota, and I. Potapov, editors, Reachability Problems - 9th International Workshop, RP 2015, Warsaw, Poland, September 21-23, 2015, Proceedings, volume 9328 of Lecture Notes in Computer Science, pages 20–32. Springer, 2015.
  8. A. Methni, M. Lemerre, B. Ben Hedia, S. Haddad, and K. Barkaoui. State space reduction strategies for model checking concurrent C programs. In Proceedings of the 9th Workshop on Verification and Evaluation of Computer and Communication Systems(VECoS’15), volume 1431 of CEUR Workshop Proceedings, pages 65–76, Bucharest, Romania, Sept. 2015.
  9. B. Bérard, S. Haddad, A. Jovanovic and D. Lime. Interrupt Timed Automata with Auxiliary Clocks and Parameters. Fundamenta Informaticae 143, 2016.

2014

  1. A. Ben Salem, A. Duret-Lutz, F. Kordon, and Y. Thierry-Mieg. Symbolic Model Checking of stutter invariant properties Using Generalized Testing Automata. In 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), volume 8413 of Lecture Notes in Computer Science, pages 440–454, Grenoble, France, April 2014. Springer
  2. S. Baarir and A. Duret-Lutz. Mechanizing the minimization of deterministic generalized büchi automata. In 34th IFIP International Conference on Formal Techniques for Distributed Objects, Components and Systems – DisCoTec, volume 8461 of Lecture Notes in Computer Science, page 266-283. Springer, 2014.
  3. É. André, F. Kordon, and L. Petrucci. Teaching formal methods: Experience at UPMC and UP13 with CosyVerif. pages 31–34. IEEEE, May 2014.
  4. A. Methni, M. Lemerre, B. Ben Hedia, S. Haddad and K. Barkaoui. Specifying and Verifying Concurrent C Programs with TLA+. In Proceeding of the the 3rd International Workshop on Formal Techniques for Safety-Critical Systems (FTSCS'14). To appear in Communications in Computer and Information Science
  5. A. Methni, M. Lemerre, B. Ben Hedia, S. Haddad and K. Barkaoui. An Approach for Verifying Concurrent C Programs. In Proceeeding of the 8th Junior Researcher Workshop on Real-Time Computing. pages 33-36, Versailles, France, 2014
  6. F. Kordon and F. Hulin-Hubard. BenchKit, a Tool for Massive Concurrent Benchmarking. 14th International Conference on Application of Concurrency to System Design (ACSD), pages 159-165, IEEE Computer Society, June 2014
  7. S. Baarir and F. Kordon and L. Pettruci. From Symmetric Nets to Symmetric Nets with Bags. 35th International Conference on Application and Theory of Petri Nets and Concurrency (Petri Nets), online, June 2014
  8. G. Lipari, S. Youcheng, É. André and L. Fribourg. Toward Parametric Timed Interfaces for Real-Time Components. In É. André and G. Frehse (eds.), SynCoP’14, EPTCS 145, pages 49–64, April
    2014.

2013

  1. L.Fronc and A.Duret-Lutz. LTL model checking with Neco. In Proceedings of the 11th International Symposium on Automated Technology for Verification and Analysis (ATVA’13), volume 8172 of Lecture Notes in Computer Science, pages 451–454, Hanoi, Vietnam, Oct. 2013. Springer.
  2. F. Kordon, A. Linard, M. Becutti, D. Buchs, L. Fronc, F. Hulin-Hubard, F. Legond-Aubry, N. Lohmann, A. Marechal, E. Paviot-Adet, F. Pommereau, C. Rodrigues, C. Rohr, Y. Thierry-Mieg, H. Wimmel, and K. Wolf. Model Checking Contest @ Petri Nets, Report on the 2013 edition. Technical report, CoRR, September 2013.
  3. S. Haar, S. Haddad, T. Melliti and S. Schwoon. Optimal Constructions for Active Diagnosis. In FSTTCS'13, Leibniz International Proceedings in Informatics 24, pages 527-539. Leibniz-Zentrum für Informatik, 2013
  4. B. Bérard, S. Haddad, A. Jovanovic and D. Lime. Parametric Interrupt Timed Automata. In RP'13, LNCS 8169, pages 59-69. Springer, 2013.
  5. S. Haddad, L. Mokdad and S. Youcef. Bounding models families for performance evaluation in composite Web services. Journal of Computational Science 4(4), pages 232-241, 2013.
  6. E. Renault, A. Duret-Lutz, F. Kordon, and D. Poitrenaud. Strength-based decomposition of the property Büchi automaton for faster model checking. In 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), volume 7795 of Lecture Notes in Computer Science, pages 565-579, Rome, Italy, March 2013. Springer.
  7. E. André, Y. Lembachar, L. Petrucci, F. Hulin-Hubard, A. Linard, L.-M. Hillah, and F. Kordon. CosyVerif : an Open Source Extensible Verification Environment. In 18th IEEE International Con- ference on Engineering of Complex Computer Systems – ICECCS, page to be published, Singapore, July 2013. IEEE Computer Society.
  8. B. Bérard, F. Cassez, S. Haddad, D. Lime, and O. H. Roux. The Expressive Power of Time Petri Nets. Theoretical Computer Science, 474:1–20, Feb. 2013.
  9. J-M. Delosme, T. Hujsa, A. Munier-Kordon. Polynomial Sufficient Conditions of Well-Behavedness for Weighted Join-Free and Choice-Free Systems. In Proceedings of the 13th Int. Conf. on Application of Concurrency to System Design (ACSD'13), Barcelona, Spain, pages 90 - 99. IEEE Computer Society, July 2013.
  10. S. Youcheng, R. Soulat, G. Lipari, É. André and L. Fribourg. Parametric Schedulability Analysis of Fixed Priority Real-Time Distributed Systems. In Cyrille Artho and Peter Ölveczky (eds.), FTSCS'13, CCIS, Springer, October 2013
  11. É. André, L. Fribourg and R. Soulat. Merge and Conquer: State Merging in Parametric Timed Automata. In Hung Dang-Van and Mizuhito Ogawa (eds.), ATVA'13, LNCS 8172, Springer, pages 381–396, October 2013.
  12. E. Renault, A. Duret-Lutz, F. Kordon, and D. Poitrenaud. Three SCC-based Emptiness Checks for Generalized Büchi Automata. In 19th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning – LPAR, volume 8312 of Lecture Notes in Computer Science, page 668-682, Stellen- bosch, South Africa, December 2013. Springer.

2012

  1. B. Bérard, S. Haddad and M. Sassolas. Interrupt Timed Automata: verification and expressiveness. Formal Methods in System Design 40(1), pages 41-87, 2012.
  2. F. Kordon, A. Linard, D. Buchs, M. Colange, S. Evangelista, L. Fronc, L.-M. Hillah, N. Lohmann, E. Paviot-Adet, F. Pommereau, C. Rohr, Y. Thierry-Mieg, and K. Wolf. Raw Report on the Model Checking Contest at Petri Nets 2012. Technical report, CoRR, September 2012
  3. S. Hong, F. Kordon, E. Paviot-Adet and S. Evangelista. Computing a Hierarchical Static order for Decision Diagram-Based Representation from P/T Nets. Transactions on Petri Nets and Other Models of Concurrency (ToPNoC), VI:121-140, Springer Verlag, march 2012.
  4. F. Kordon, A. Linard, D. Buchs, M. Colange, S. Evangelista, K. Lampka, N. Lohmann, E. Paviot- Adet, Y. Thierry-Mieg, and H. Wimmel. Report on the Model Checking Contest at Petri Nets 2011. Transactions on Petri Nets and Other Models of Concurrency (ToPNoC), VI:169-196, 2012.
  5. B. Bérard, S. Haddad, M. Sassolas, and N. Sznajder. Concurrent Games on VASS with Inhibition. In Proceedings of the 23rd Int. Conf. on Concurrency Theory (CONCUR’12, pages 39–52, Newcastle, England, September 2012.
  6. J. Delange, L. Pautet and F. Kordon. Design, implementation and verification of MILS systems. Software Practice and Experience, 42(7), pages 799-816, Wiley, 2012.
  7. L.M. Hillah, F. Kordon, C. Lakos and L. Petrucci. Extending PNML Scope: a Framework to Combine Petri Nets Types. Transactions on Petri Nets and Other Models of Concurrency (ToPNoC), VI, pages 46-70, Springer Verlag, 2012.
  8. A.E. Ben Salem, A. Duret-lutz and F. Kordon. Model Checking using Generalized Testing Automata. Transactions on Petri Nets and Other Models of Concurrency (ToPNoC), VI, pages 94-122, Springer Verlag, 2012.
  9. M. Jan, C. Jouvray, F. Kordon, A. Kung, J. Lalande, Frédéric Loiret, J. Navas, L. Pautet, J. Pulou, A. Radermacher and L. Seinturier. Flex-eWare: a Flexible Solution for Designing and Implementing Embedded Distributed Systems. Software Practice and Experience, 42(12), pages 1467-1794, Wiley, 2012.
  10. A.-E. Ben Salem, A. Duret-lutz, and F. Kordon. Model Checking using Generalized Testing Automata. Transactions on Petri Nets and Other Models of Concurrency (ToPNoC), VI:94–122, 2012.
  11. F. Gava, M. Guedj, and F. Pommereau. A BSP Algorithm for On-the-Fly Checking CTL* Formulas on Security Protocols. In 13th International Conference on Parallel and Distributed Computing, Applications and Technologies (PDCAT), pages 79–84. IEEE, 2012.
  12. F. Gava, M. Guedj, and F. Pommereau. A BSP Algorithm for On-the-fly Checking LTL Formulas on Security Protocols. In 11th International Symposium on Parallel and Distributed Computing (ISPDC), pages 11–18. IEEE Computer Society, 2012.
  13. F. Gava, M. Guedj, and F. Pommereau. Performance Evaluations of a BSP Algorithm for State Space Construction of Security Protocols. In Proceedings of the 20th Euromicro International Conference on Parallel, Distributed and Network-Based Processing (PDP), pages 170–174. IEEE, 2012.
  14. É. André, L. Fribourg, U. Kühne and R. Soulat. IMITATOR 2.5: A Tool for Analyzing Robustness in Scheduling Problems. In Dimitra Giannakopoulou and Dominique Méry (eds.), FM’12, LNCS 7436, Springer, pages 33–36, August 2012
  15. É. André, L. Fribourg and R. Soulat. Enhancing the Inverse Method with State Merging. In Alwyn Goodloe and Suzette Person (eds.), NFM’12, LNCS 7226, Springer, pages 100–105, April 2012

2011

  1. K. Barkaoui, B. Monsuez, D. Poitrenaud : "Editorial - Special Issue on Verification and Evaluation of Computer and Communication Systems – Part I" In Int. J. Critical Computer-Based Systems (IJCCBS), Vol. 2, Nos. 3/4, 2011, pp. 217-220 (ISSN : 1757-2703)
  2. P. Ballarini, H. Djafri, M. Duflot, S. Haddad and N. Pekergin. COSMOS: a Statistical Model Checker for the Hybrid Automata Stochastic Logic. in proceedings of QEST'11. pp 143-144, IEEE Computer Society Press, 2011
  3. P. Ballarini, H. Djafri, M. Duflot, S. Haddad and N. Pekergin. Petri Nets Compositional Modeling and Verification of Flexible Manufacturing Systems. in proceedings of CASE'11. IEEE Robotics & Automation Society, 2011.
  4. L.M. Hillah, F. Kordon, C. Lakos, and L. Petrucci. Extending PNML Scope : the Prioritised Petri Nets Experience. Petri Net and Software Engineering (PNSE 2011), vol 723, pages 61-75, CEUR, June 2011
  5. A. E. Ben Salem, A. Duret-Lutz, and F. Kordon. Generalized Büchi automata versus testing automata for model checking. In 2nd International Workshop on Scalable and Usable Model Checking for Petri Net and other models of Concurrency (SUMO’11), volume 626 of Workshop Proceedings, Newcastle, UK, June 2011. CEUR.
  6. P. Ballarini, H. Djafri, M. Duflot, S. Haddad and N. Pekergin. HASL: An Expressive Language for Statistical Verification of Stochastic Models. In VALUETOOLS'11. 2011. To appear.
  7. S. Baarir, M. Beccuti, C. Dutheillet, G. Franceschinis and S. Haddad. Lumping partially symmetrical stochastic models. Performance Evaluation 76, pages 21-44, 2011.
  8. J. Delange, L.Pautet, and F. Kordon. Reconfigurable Embedded Control Systems : Applications for Flexibility and Agility, chapter A Model-Based Approach To Configure and Reconfigure Avionics Systems, pages 509–541. Number 19. IGI Global, 2011.
  9. É. André and R. Soulat. Synthesis of Timing Parameters Satisfying Safety Properties. In Giorgio Delzanno and Igor Potapov (eds.), RP’11, LNCS 6945, Springer, pages 31–44, 2011

2010

  1. B. Bérard, S. Haddad and M. Sassolas. Real Time Properties for Interrupt Timed Automata. In TIME'10. pages 69-76, IEEE Computer Society Press, Paris, September 2010.
  2. S. Haddad, L. Mokdad and S. Youcef. Response time of BPEL4WS constructors. In IEEE Symposium on Computer and Communications (ISCC'10). IEEE Computer Society Press, June 2010.
  3. J. Delange, L. Pautet, and F. Kordon. Design, Verification and Implementation of MILS systems. In Proceedings of the 21th International Symposium on Rapid System Prototyping, page 1-8, Fairfax, June 2010. IEEE Computer Society.
  4. C. Choppy, A. Dedova, S. Evangelista, S. Hong, K. Klai, and L. Petrucci. The NEO protocol for large-scale distributed database systems : Modelling and initial verification. volume 6128, pages 145–164, June 2010.
  5. L. Hillah, F. Kordon, L. Petrucci, and N. Trèves. PNML Framework : an extendable reference implementation of the Petri Net Markup Language. In 31st International Conference on Petri Nets and Other Models of Concurrency (ICATPN 2010), volume 6128 of Lecture Notes in Computer Science, pages 318-327, Braga, Portugal, June 2010. Springer.
  6. L. Hillah and L. Petrucci. Standardisation des réseaux de Petri : état de l’art et enjeux futurs. Revue Génie Logiciel, 93 :5–10, June 2010.
  7. G. Lasnier, T. Robert, L. Pautet, and F. Kordon. Behavioral Modular Description of Fault Tolerant Distributed Systems with AADL Behavioral Annex. In 10st international conference on New Technologies of Distributed Systems (NOTERE'2010), page ??, Tozeur, Tunisia, June 2010. IEEE Computer Society.
  8. G. Lasnier, T. Robert, L. Pautet, and F. Kordon. Architectural and Behavioral Modeling with AADL for Fault Tolerant Embedded Systems. In 13th IEEE International Symposium on Object-oriented Real-time distributed Computing (ISORC'10), pages 87-91, Carmona, Spain, May 2010. IEEE Computer Society.
  9. J. Delange, L. Pautet, and F. Kordon. Modeling and Validation of ARINC653 architectures. In Embedded Real Time Software and Systems (ERTSS'10), pages 1-8, Toulouse, France, May 2010.
  10. S. Haddad, L. Mokdad et S. Youcef Response time of BPEL4WS constructors, IEEE Symposium on Computers and Communications (ISCC'10), Riccione, Italie, Juin 2010.
  11. H. Bel mokadem, B. Bérard, V. Gourcuff, J.-M. Roussel and P. De Smet, Verification of a Timed Multitask System with Uppaal (2010), in: IEEE Transactions on Automation Science and Engineering (T-ASE), 7:4(921-932)

2009

  1. L. Hillah, E. Kindler, F. Kordon, L. Petrucci, and N. Trèves. A primer on the Petri Net Markup Language and ISO/IEC 15909-2. In 10th International workshop on Practical Use of Colored Petri Nets and the CPN Tools (CPN’09), page 9-28, 2009.
  2. S. Haddad, F. Kordon, L. Petrucci, J-F. Pradat-Peyre, and N. Trèves. Efficient State-Based Analysis by Introducing Bags in Petri Net Color Domains. 28th American Control Conference (ACC'09), pages 5018-5025, Omnipress IEEE Catalog, June 2009.
  3. X. Renault, F. Kordon, and J. Hugues. Adapting models to model checkers, a case study: Analysing AADL using Time or Colored Petri Nets. Proceedings of the 20th International Workshop on Rapid System Prototyping, pages 26-33, IEEE Computer Society, June 2009.
  4. Haddad and N. Pekergin Using Stochastic Comparison for Efficient Model Checking of Uncertain Markov Chains In QEST'09. IEEE Computer Society. pages 177-186, May 2009.
  5. B. Bérard and S. Haddad. Interrupt Timed Automata. In FoSSaCS'09, LNCS 5504, pages 197-211. Springer, March 2009.
  6. X. Renault, F. Kordon, and J. Hugues. From AADL architectural models to Petri Nets: Checking model viability. 12th IEEE International Symposium on Object-oriented Real-time distributed Computing (ISORC'09), pages 313-320, IEEE Computer Society, March 2009.
  7. F. Pommereau, R. Devillersn H. Klaudel. Efficient Reachability Graph Representation of Petri Nets With Unbounded Counters. Electr. Notes Theor. Comput. Sci. 239:119-129, 2009.
  8. O. Bertrand, A. Calonne, C. Choppy, S. Hong, K. Klai, F. Kordon, Y. Okuji, E. Paviot-Adet, L. Petrucci and J.-P. Smets. Verification of large-scale distributed database systems in the NEOPPOD project. Workshop on Petri Nets and Software Engineering (PNSE'09, associated with Petri Nets 2009) - poster paper, pages 315-316, June 2009.
  9. X. Renault, F. Kordon, and J. Hugues. Adapting models to model checkers, a case study: Analysing AADL using Time or Colored Petri Nets. Proceedings of the 20th International Workshop on Rapid System Prototyping, pages 26-33, IEEE Computer Society, June 2009.
  10. An Approach to State Space Reduction for Systems with Dynamic Process Creation. Hanna Klaudel, Maciej Koutny, Elisabeth Pelz and Franck Pommereau. Proc. of ISCIS'09, IEEE Press, pages 543-548, September 2009.
  11. L. Hillah, E. Kindler, F. Kordon, L. Petrucci and N. Trèves. A primer on the Petri Net Markup Language and ISO/IEC 15909-2 (originally presented at the 10th International workshop on Practical Use of Colored Petri Nets and the CPN Tools - CPN'09). Petri Net Newsletter, 76, pages 9-28, Gesellschaft für Informatik, October 2009.
  12. J. Delange, L. Pautet, A. Pantec, M. Kerboeuf, F. Singhoff and F. Kordon. Validate, Simulate, and Implement ARINC653 Systems Using the AADL. ACM SIGAda Ada Letters (from the proceedings of the ACM SigAda conference 2009), 29(3), pages 31-44, ACM Press, November 2009.
  13. F. Bonnefoi, C. Choppy and F. Kordon. A Discretization Method from Coloured to Symmetric Nets: Application to an Industrial Example. Transactions on Petri Nets and Other Models of Concurrency (ToPNoC), III, pages 159-188, Springer Verlag, November 2009.
  14. A. Duret-Lutz, D. Poitrenaud, and J.-M. Couvreur. On-the-fly emptiness check of transition-based Streett automata. In Z. Liu and A. P. Ravn, editors, Proceedings of the 7th International Symposium on Automated Technology for Verification and Analysis (ATVA’09), volume 5799 of LNCS, pages 213–227. Springer-Verlag, 2009.

2008

  1. H. Klaudel and F. Pommereau. M-nets: a survey. Acta Informatica 236(7), Springer Verlag, October 2008.
  2. F. Kordon, J. Hugues, and X. Renault. From Model Driven Engineering to Verification Driven Engineering. In 6th IFIP Workshop on Software Technologies for Future Em- bedded & Uiquitous Systems (SEUS 2008), volume 5287 of Lecture Notes in Computer Science, pages 381-393, Capri, Italy, October 2008. Springer.
  3. H. Klaudel, M. Koutny, E. Pelz, F. Pommereau. Towards Efficient Verification of Systems with Dynamic Process Creation. ICTAC 2008, pp 186-200, September 2008.
  4. J. Hugues, B. Zalila, L. Pautet, F. Kordon : "From the Protoype to the Final Embedded System Using the Ocarina AADL Tool Suite", Transactions on Embedded Computing System, 7(4) :1-25, July 2008.
  5. L. Hillah, F. Kordon, L. Petrucci : "Application des méthodes formelles à la robotique modulaire", Journal Européen des Systèmes Automatisés, vol. 42, pp. 459-478, May 2008.
  6. B. Bérard, S. Haddad, L. Hillah, F. Kordon, Y. Thierry-Mieg : "Applying Control Theory to Collision Avoidance in Intelligent Transport Systems", 9th International Workshop on Discrete Event Systems (WODES'08), pages 346-351, Goteborg, Sweden, May 2008. IEEE Press.
  7. K. Klai, D. Poitrenaud : "MC-SOG: An LTL Model Checker Based on Symbolic Observation Graphs", 29th International Conference on Application and Theory of Petri Nets (ICATPN'08), Lecture Notes in Computer Science (LNCS), Xian, China, pp. 288-306, (Springer-Verlag), June 2008.
  8. X. Renault, J. Hugues, F. Kordon : "Formal Modeling of a Generic Middleware to Ensure Invariant Properties", 10th Formal Methods for Open Object-based Distributed Systems (FMOODS'08), Lecture Notes in Computer Science (LNCS), Oslo, Norway, pp. 185-200, (Springer-Verlag).
  9. Modeling and analysis of security protocols using role based specifications and Petri nets.
    Roland Bouroulet, Raymond Devillers, Hanna Klaudel, Elisabeth Pelz and Franck Pommereau
    Proc. of ICATPN'08, LNCS 5062, Springer, pp 72-91, (Springer-Verlag).
  10. B. Bérard, F. Cassez, S. Haddad, D. Lime and O. H. Roux. When are Timed Automata Weakly Timed Bisimilar to Time Petri Nets? Theoretical Computer Science 403(2-3), pages 202-220, 2008.
  11. A. Hamez, L. Hillah, K. Klai, F. Kordon, L. Petrucci, D. Poitrenaud, and Y. Thierry-Mieg. CoSyVerif: Complex Systems Verification, June 2008. Tool presentation at PetriNets’08.
  12. S. Haddad, L. Mokdad et S. Youcef Response time analysis for compositeWeb services, 6th IEEE Symposium on Communication Systems, Networks and Digital Signal Processing, (CNDSPS'08), pp. 1-5, Graz, juillet 2008.
  13. H.Castel, L.Mokdad et N. Pekergin Model checking of performance measures using bounding aggregations, IEEE International Symposium on Performance Evaluation of Computer and Telecommunication Systems, (SPECTS'08), pp. 1-7, Edinburgh, UK, juin 2008.

2007

  1. S. Haddad, D. Poitrenaud : "Recursive Petri nets - Theory and application to discrete event systems", Acta Informatica, vol. 44, pp. 463-508.
  2. J. Hugues, B. Zallila, L. Pautet, F. Kordon : "Rapid Prototyping of Distributed Real-Time Embedded Systems Using the AADL and Ocarina", 18th International Workshop on Rapid System Prototyping (RSP), Porto Alegre, Brazil, pp. 106-112.
  3. J. Hugues, F. Kordon, L. Pautet, Th. Vergnaud : "A Factory To Design and Build Tailorable and Verifiable Middleware", Workshop on Networked Systems: Realization of Reliable Systems on Top of Unreliable Networked Platforms (Monterey Workshop Series, 12th edition, 2005), Lecture Notes in Computer Science (LNCS), University of California, Irvine, USA, pp. 123-144, (Springer-Verlag).
  4. F. Kordon and L. Petrucci : "A formal approach to designing autonomous systems : from Intelligent Transport Systems to robots", 2nd National Workshop on Control Architectures of Robots : from models to execution on distributed control architectures, Paris, France.
  5. F. Pommereau, R. Devillers and H. Klaudel, Efficient reachability graph representation of Petri nets with unbounded counters. Proc. of Infinity'07, ENTCS, Elsevier, pp 1-10.
  6. H.Castel, L.Mokdad et N. Pekergin Stochastic bounds applied to the end to end QoS in communication systems, 15th IEEE International Symposium on Modeling, Analysis, and Simulation of Computer and Telecommunication (MASCOTS'07), Istambul, Turquie, pp. 374-380, octobre 2007.
  7. H.Castel, L.Mokdad et N. Pekergin Aggregated bounding Markov processes applied to the analysis of tandem queues, 2nd ACM International Conference on Performance Evaluation Methodologies and Tools (VALUETOOLS'07), Nantes, France, pp. 1-10, octobre 2007.
  8. S. Baarir and A. Duret-Lutz. Emptiness check of powerset Büchi automata. In Proceedings of the 7th International Conference on Application of Concurrency to System Design (ACSD’07), pages 41–50. IEEE Computer Society, July 2007.

2006

  1. F. Kordon, L. Petrucci : "Toward Formal-Methods Oecumenism?", IEEE Distributed Systems Online, vol. 7.
  2. S. Haddad, F. Kordon, L. Petrucci : "Introduction générale", Méthodes formelles pour les systèmes répartis et coopératifs, Haddad Serge, Kordon Fabrice, Petrucci Laure, pp. 1-6, (ISBN : 2-7462-1447-4).
  3. J. Hugues, F. Kordon, L. Pautet : "Construction d'un intergiciel vérifié", dans Méthodes formelles pour les systèmes répartis et coopératifs, édité par Haddad Serge, Kordon fabrice, Petrucci Laure, pp. 265-287, (Hermes), (ISBN : 2-7462-1447-4).
  4. L. Hillah, F. Kordon, L. Petrucci, N. Trèves : "PN Standardisation : a Survey", International Conference on Formal Methods for Networked and Distributed Systems (FORTE '06), Lecture Notes in Computer Science (LNCS), Paris, France, pp. 307-322, (Springer-Verlag).
  5. J. Hugues, F. Kordon, L. Pautet : "A Framework for DRE Middleware, an Application to DDS", International Symposium on Object-Oriented Real-time Distributed Computing (ISORC'06), Gyeongju, Korea, pp. 224-231.
  6. K. Barkaoui, J.F Pradat-Peyre : "Approches structurelles", Chapitre 7 dans Méthodes formelles pour les systèmes répartis et coopératifs, édité par Haddad Serge, Kordon fabrice, Petrucci Laure, pp. 265-287, (Hermes), (ISBN : 2-7462-1447-4).
  7. C. Choppy, S. Haddad, H. Klaudel, F. Kordon, L. Petrucci, and Y. Thierry-Mieg. Tutorial on formal methods for distributed and cooperative systems. In Proc. 3rd Int. Coll. on Theoretical Aspects of Computing (1-day tutorial at ICTAC’06), Tunis, Tunisia, volume 4281, pages 362–365, Nov. 2006

2005

  1. L. Hillah, F. Kordon, L. Petrucci, N. Trèves : "Model Engineering on Petri Nets for ISO/IEC 15909-2: API Framework for Petri Net Types Metamodels", Petri Net Newsletter, pp. 22-40.
  2. F. Kordon, L. Pautet : "Toward next-generation toward next-generation middleware ?", IEEE DIstributed Systems Online, vol. 5.
  3. J. Hugues, L. Pautet, F. Kordon : "Revisiting COTS Middleware for DRE System", International Symposium on Object-Oriented Real-time Distributed Computing (ISORC '05), Seattle, USA, pp. 72-79.
  4. J. Hugues, F. Kordon, L. Pautet : "Towards Proof-Based Real-Time Distribution Middleware", 13th International Conference On Real-Time Systems (RTS '05), Paris, France, pp. 51-70, (BIRP).
  5. K. Klai, S. Haddad, J.-M. Ilié : "Modular Verification of Petri Nets Properties: A Structure-Based Approach", 25th IFIP International Conference on Formal Techniques for Networked and Distributed Systems (FORTE'05), Lecture Notes in Computer Science (LNCS), Taipei, Taïwan, pp. 189-203, (Springer-Verlag).
  6. Th. Vergnaud, L. Pautet, F. Kordon : "Using the AADL to Describe Distributed Applications from Middleware to Software Components", Reliable Software Technologies (RST'05), York, United Kingdom, pp. 67-78.
  7. K. Barkaoui, J.M. Couvreur, Kaïs Klaï "On the Equivalence Between Liveness and Deadlock-Freeness in Petri Nets" 26th International Conference Applications and Theory of Petri Nets (ICATPN'05), Lecture Notes in Computer Science (LNCS) Vol. 3536, 2005, pp. 90-107, (Springer)
  8. J.-M. Couvreur, A. Duret-Lutz, and D. Poitrenaud. On-the-fly Emptiness Checks for Generalized Büchi automata. In Model Checking Software, 12th International SPIN Workshop, volume 3639 of LNCS, pages 169–184, 2005.