Répertoire des expertises

Vous êtes ici

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

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
Communication de conférence
Helouet, L., Marchand, H. & Mullins, J. (2018). Concurrent Secrets with Quantified Suspicion. Communication présentée à 18th International Conference on Application of Concurrency to System Design (ACSD 2018), Bratislava, Slovakia (p. 75-84). Tiré de https://doi.org/10.1109/ACSD.2018.00011
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

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 https://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 https://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 https://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 https://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 https://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).