Répertoire des expertises

Vous êtes ici

Retour aux résultats de recherche
John Mullins
B.Sc., M.Sc. (Montréal), Ph.D. (INRS)

Tél. : (514) 340-4711 poste 3278 Téléc. : (514) 340-5139 Local : M-4101

Intérêts de recherche et affiliations

Intérêts de recherche

Méthodes formelles de spécification et de vérification des systèmes concurrents et de la sécurité des systèmes d'information.

  • Méthode formelle

  • Analyse des systèmes

  • Analyse de la sécurité

  • Modèle et calcul des systèmes concurrents

  • Description et vérification des systèmes

  • Systèmes concurrents orientés objet

  • Système concurrents mobiles

  • Modèle et vérification pour la sécurité dse systèmes

Affiliation(s)
Type(s) d'expertises (sujets CRSNG)
  • 2700 TECHNOLOGIE DE L'INFORMATION
  • 2710 Conception de systèmes d'information
  • 2713 Algorithmes
  • 2714 Mathématiques de l'informatique

Publications

Publications récentes
Article de revue
Bérard, B., Kouchnarenko, O., Mullins, J. & Sassolas, M. (2018). Opacity for linear constraint Markov chains. Discrete Event Dynamic Systems: Theory and Applications, 28(1), 83-108. Tiré de https://doi.org/10.1007/s10626-017-0259-4
Article de revue
Robati, T., Gherbi, A., El Kouhen, A. & Mullins, J. (2017). Design and simulation of distributed IMA architectures using TTEthernet: a model-driven approach. Journal of Ambient Intelligence and Humanized Computing, 8(3), 345-355. Tiré de https://doi.org/10.1007/s12652-017-0449-9
Communication de conférence
Robati, T., Gherbi, A. & Mullins, J. (2016). A modeling and verification approach to the design of distributed ima architectures using TTEthernet. Communication présentée à 7th International Conference on Ambient Systems, Networks and Technologies (ANT2016) and 6th International Conference on Sustainable Energy Information Technology (SEIT2016), Madrid, Spain (p. 229-236). Tiré de https://doi.org/10.1016/j.procs.2016.04.120
Chapitre de livre
Hamadou, S., Mullins, J. & Gherbi, A. (2016). A real-time concurrent constraint calculus for analyzing avionic systems embedded in the IMA connected through TTethernet. Dans Theoretical Information Reuse and Integration (Vol. 446, p. 85-111). Tiré de https://doi.org/10.1007/978-3-319-31311-5_4

Enseignement

Requis et spécification de logiciels. Méthodes formelles de validation de logiciels. Spécification et vérification des protocoles de communication.

Encadrement à Polytechnique

TERMINÉ

  • Thèse de doctorat (3)

    • Abouzaid, M.F. (2010). Analyse formelle d'orchestrations de services Web (Thèse de doctorat, École Polytechnique de Montréal). Tiré de http://publications.polymtl.ca/445
    • Hamadou, S. (2008). Analyse formelle des protocoles cryptographiques et flux d'information admissible (Thèse de doctorat, École Polytechnique de Montréal).
    • Lafrance, S. (2005). Spécification et validation de protocoles de sécurité (Thèse de doctorat, École Polytechnique de Montréal).
  • Mémoire de maîtrise (7)

    • Dupeuble, G. (2017). Préservation de l'opacité par raffinement de systèmes spécifiés par des chaînes de Markov discrètes à intervalles (Mémoire de maîtrise, École Polytechnique de Montréal). Tiré de http://publications.polymtl.ca/2569/
    • Nleng, C.H. (2014). Modélisation et vérification du flux d'information pour les systèmes orientés objets (Mémoire de maîtrise, École Polytechnique de Montréal). Tiré de http://publications.polymtl.ca/1549
    • Khadem Mohtaram, A. (2013). Classification, Formalization and Automatic Verification of Untraceability in RFID Protocols (Mémoire de maîtrise, École Polytechnique de Montréal). Tiré de http://publications.polymtl.ca/1094
    • Kiraga, A.F. (2010). Vérification des systèmes de sécurité probabilistes : restriction de l'attaquant (Mémoire de maîtrise, École Polytechnique de Montréal). Tiré de http://publications.polymtl.ca/349
    • Oarga, R.-M. (2005). Vérification à la volée de contraintes OCL étendues sur des modèles UML (Mémoire de maîtrise, École Polytechnique de Montréal).
    • Bastien, G. (2004). ASPiC : un outil d'analyse symbolique automatisée de protocoles cryptographiques basé sur le modèle de flux d'information (Mémoire de maîtrise, École Polytechnique de Montréal).
    • Bergeron, M. (2004). Model-checking UML designs using a temporal extension of the object constraint language (Mémoire de maîtrise, École Polytechnique de Montréal).