Publications on Cosmos

  1. B. Barbot, B. Bérard, Y. Duplouy and S. Haddad.  Integrating Simulink Models into the Model Checker Cosmos.  In Proceedings of the 39th International Conference on Applications and Theory of Petri Nets (PETRI NETS'18), pages 363-373, Bratislava, Slovakia, June 2018, LNCS. Springer.
  2. 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 90, pages 53-77, 2015.
  3. P. Ballarini, H. Djafri, M. Duflot, S. Haddad and N. Pekergin.  COSMOS: a Statistical Model Checker for the Hybrid Automata Stochastic Logic.  In QEST'11, pages 143-144. IEEE Computer Society Press, 2011.
  4. P. Ballarini, H. Djafri, M. Duflot, S. Haddad and N. Pekergin.  HASL: An Expressive Language for Statistical Verification of Stochastic Models.  In VALUETOOLS'11, pages 306-315. 2011.

Publications using Cosmos

  1. B. Barbot, N. Basset and T. Dang. Generation of signals under temporal constraints for CPS testing.  In NASA Formal Methods 11th International Symposium, NFM 2019, Houston, TX, USA, May 7-9, 2019, Proceedings, volume 11460 of Lecture Notes in Computer Science, pages 54-70. Springer, 2019. 2019.
  2. P. Ballarini, B. Barbot, N. Vasselin. Performance modelling of access control mechanisms for local and vehicular wireless networks.. In Proceedings of the 12th EAI International Conference on Performance Evaluation Methodologies and Tools, VALUETOOLS 2019, pages 111 118. ACM, 2019.
  3. B. Barbot, B. Bérard, Y. Duplouy, and S. Haddad. Statistical model-checking for autonomous vehicle safety validation. In SIA Simulation Numérique, 2017.
  4. P. Ballarini, M. Beccuti, Enrico Bibbona, Andras Horvath, Roberta Sirovich, Jeremy Sproston.  Analysis of Timed Properties Using the Jump-Diffusion Approximation.  In proceedings of the 14th European Performance Engineering Workshop (EPEW 2017). 2017.
  5. B. Barbot, N. Basset, M. Beunardeau and M. Kwiatkowska.  Uniform Sampling for Timed Automata with Application to Language Inclusion Measurement.  In QEST'16, volume 9826 of Lecture Notes in Computer Science, pages 175–190. Springer, 2016.
  6. B. Barbot, M. Kwiatkowska, A. Mereacre and N. Paoletti.  Building Power Consumption Models from Executable Timed I/O Automata Specifications.  In HSCC'16, pages 195–204. ACM, 2016.2016.
  7. B. Barbot, M. Kwiatkowska, A. Mereacre and N. Paoletti.  Estimation and verification of hybrid heart models for personalised medical and wearable devices.  In CMSB'15, volume 9308 of LNCS, pages 3-7. 2015.
  8. P. Ballarini and M. Duflot.  Applications of an expressive statistical model checking approach to the analysis of genetic circuits.  In Theoretical Computer Science, Elsevier, DOI, 06/2015.
  9. B. Barbot, S. Haddad, M. Heiner and C. Picaronny.  A Rare Event Method Applied to Signalling Cascades.  International Journal on Advances in Systems and Measurements 8(1-2), 2015.
  10. B. Barbot and M. Kwiatkowska.  On Quantitative Modelling and Verification of DNA Walker Circuits Using Stochastic Petri Nets.  In ICATPN'15, LNCS 9115, pages 1-32. Springer, 2015.
  11. P. Ballarini, Analysing oscillatory trends of discrete-state stochastic processes through HASL statistical model checking.  In STTT, 17(4):505–526, 2015.
  12. B. Barbot, S. Haddad, M. Heiner and C. Picaronny.  Rare Event Handling in Signalling Cascades.  In SIMUL'14, pages 126-131. XPS, 2014.
  13. P. Ballarini, E. Gallet, P. Le Gall, and M. Manceny.  Formal analysis of the Wnt/beta-catenin pathway through statistical model checking. In proceedings of 6th Int. Symposium On Leveraging Applications of Formal Methods, Verification and Validation (ISOLA), 2014, pag. 193-207.
  14. G. Amparore, P. Ballarini, M. Beccuti, S. Donatelli and G. Franceschinis.  Expressing and computing passage time measures of gspn models with hasl. In proceedings of 34th Int. Conf. Petri Nets, 2013, pag. 110-129,
  15. G. Amparore, B. Barbot, M. Beccuti, S. Donatelli and G. Franceschinis.  Simulation-based Verification of Hybrid Automata Stochastic Logic Formulas for Stochastic Symmetric Nets.  In PADS'13, pages 253-264. ACM Press, 2013.
  16. B. Barbot, S. Haddad and C. Picaronny.  Importance Sampling for Model Checking of Continuous Time Markov Chains.  In SIMUL'12, pages 30-35. XPS, 2012.
  17. B. Barbot, S. Haddad and C. Picaronny.  Coupling and Importance Sampling for Statistical Model Checking.  In TACAS'12, LNCS 7214, pages 331-346. Springer, 2012.
  18. P. Ballarini, J. Makkela and S. Ribeiro .  Expressive Statistical Model Checking of Genetic Networks with Delayed Stochastic Dynamics.  In proceedings of 10th Int. Conf. on Computational Methods in Systems Biology (CMSB), 2012, London, UK. Springer Berlin Heidelberg, Lecture Notes in Computer Science, pag. 29-48.
  19. B. Barbot, S. Haddad and C. Picaronny.  Échantillonnage préférentiel pour le model checking statistique.  In MSR'11, Journal Européen des Systèmes Automatisés 45(1-3), pages 237-252. Hermès, 2011.
  20. P. Ballarini, H. Djafri, M. Duflot, S. Haddad and N. Pekergin.  Petri Nets Compositional Modeling and Verification of Flexible Manufacturing Systems.  In proceedings of 7th Annual IEEE Conference on Automation Science and Engineering (CASE 2011). IEEE. DOI: 10.1109/CASE.2011.6042488, pag. 588-593.
  21. P. Ballarini, M.L. Guerriero.  Query-based Verification of Qualitative Trends and Oscillations in Biochemical Systems.  In Theoretical Computer Science.  2010, Volume 411, Issue 20, 28 April 2010, Pages 2019-2036.