L’équipe « Systèmes Sûrs » consacre ses recherches à la spécification, la conception, la vérification et l’évaluation des systèmes, en particulier des applications critiques du point de vue de la sûreté et de la sécurité. L’objectif est de développer des méthodes, techniques et outils permettant d’énoncer les propriétés recherchées pour des applications et de démontrer que ces applications satisfont les propriétés attendues. Toutes les recherches menées dans notre équipe rentrent dans le cadre général des méthodes formelles. Nos activités s’articulent autour de trois axes : l’axe « Typage, Sémantique et Preuves », l’axe « Architecture Logicielle, Architecture Système et Lignes de produits et l’axe « Vérification et Evaluation de Systèmes Parallèles et Asynchrones ».
- Annuaire
- Publications
- Anciens
- Projets
Annuaire de l'équipe
Responsable
Permanents
- Maria-Virginia Aponte (Maître de conférences)
- Kamel Barkaoui (Professeur des Universités)
- Francois Barthelemy (Maître de conférences)
- Pierre Courtieu (Maître de conférences)
- Tristan Crolard (Professeur des Universités)
- Joelle Delacroix (Maître de conférences)
- Julien Forest (Maître de conférences)
- Nicole Levy (Professeur des Universités)
- Yann Pollet (Professeur Cnam)
- Olivier Pons (Maître de conférences)
- Rachid Rebiha (Maître de conférences)
- Jean-Ferdinand Susini (Maître de conférences)
- Veronique Viguie Donzeau-Gouge (Professeur émérite)
Non Permanents
Publications
2021
Articles de revue
- Computation of an emptiable minimal siphon in a subclass of petri nets using mixed-integer programming. In IEEE/CAA Journal of Automatica Sinica: 1-8, 2021. doi www
- DevOps workflow verification and duration prediction using non-Markovian stochastic Petri nets. In Journal of Software: Evolution and Process, 2021. doi www
Non publié
- Computer Aided Formal Design of Swarm Robotics Algorithms. , working paper or preprint. www
2020
Articles de revue
- Exploiting local persistency for reduced state-space generation. In Innovations in Systems and Software Engineering, 16 (2): 181-197, 2020. doi www
- An unreliable single server retrial queue with collisions and transmission errors. In Communications in Statistics - Theory and Methods: 1-25, 2020. doi www
- Exploiting local persistency for reduced state-space generation. In Innovations in Systems and Software Engineering, 2020. doi www
- Blockchain for the Internet of Vehicles: A Decentralized IoT Solution for Vehicles Communication Using Ethereum. In Sensors, 20 (14): 3928, 2020. doi www
Articles de conférence
- Towards Efficient Partial Order Techniques for Time Petri Nets. In 14th International Conference on Verification and Evaluation of Computer and Communication Systems. VECoS 2020, pages 100-115, Xian ( virtual), France, 2020. doi www
- An Intelligent Agent-Based Industrial IoT Framework for Time-Critical Data Stream Processing. In 6th International Conference on Mobile, Secure and Programmable Networking (MSPN), 2020, pages 195-208, Paris (virtual), France, 2020. doi www
- HapiChain: A Blockchain-based Framework for Patient-Centric Telemedicine. In 2020 IEEE 8th International Conference on Serious Games and Applications for Health(SeGAH), pages 1-6, IEEE, Vancouver, Canada, 2020. doi www
- Blockchain technology for healthcare: Enhancing shared electronic health record interoperability and integrity. In 2020 IEEE International Conference on Informatics, IoT, and Enabling Technologies (ICIoT), pages 310-317, IEEE, Doha, France, 2020. doi www
- A Model-Based and Resource-Aware Testing Framework for Parking System Payment using Blockchain. In 2020 International Wireless Communications and Mobile Computing (IWCMC), pages 1252-1259, IEEE, Limassol, France, 2020. doi www
- Driver Drowsiness Detection Model Using Convolutional Neural Networks Techniques for Android Application. In 2020 IEEE International Conference on Informatics, IoT, and Enabling Technologies (ICIoT), pages 237-242, IEEE, Doha, France, 2020. doi www
- HapiFabric: A Teleconsultation Framework Based on Hyperledger Fabric. In European, Mediterranean, and Middle Eastern Conference on Information Systems, pages 399-414, Springer, Dubai, United Arab Emirates, LNBIP, vol. 402 , 2020. doi www
- A Formal Model-Based Testing Framework for Validating an IoT Solution for Blockchain-based Vehicles Communication. In 15th International Conference on Evaluation of Novel Approaches to Software Engineering, pages 595-602, SCITEPRESS - Science and Technology Publications, Prague, Czech Republic, 2020. doi www
- Du discrètement continu au contin^ument discret. In ALGOTEL 2020 -- 22èmes Rencontres Francophones sur les Aspects Algorithmiques des Télécommunications, Lyon, France, 2020. www
- Adopting Formal Verification and Model-Based Testing Techniques for Validating a Blockchain-based Healthcare Records Sharing System. In 22nd International Conference on Enterprise Information Systems, pages 261-268, SCITEPRESS - Science and Technology Publications, Prague, France, 2020. doi www
Non publié
- Formal Verification and Model-Based Testing Techniques for Validating a Blockchain-Based Healthcare Records Sharing System. , working paper or preprint. www
- Adoption de Techniques de Vérification Formelle et de Test Basé sur des Modèles pour Valider un Système de Partage de Dossiers Médicaux Basé sur la Blockchain. , working paper or preprint. www
- Un Cadre de Test Formel pour la Validation d'un Système de Communication Inter-Véhiculaire Basé sur les IOTs et la Blockchain. , working paper or preprint. www
- A Model-Based Testing Framework for Validating an IoT Solution for Blockchain-Based Vehicles Communication. , working paper or preprint. www
2019
Articles de revue
- M/M/1 Retrial Queue with Collisions and Transmission Errors. In Methodology and Computing in Applied Probability, 21 (4): 1395-1406, 2019. doi www
- Maximal Good Step Graph Methods for Reducing the Generation of the State Space. In IEEE Access, 7: 155805-155817, 2019. doi www
- Elementary Siphon-Based Robust Control for Automated Manufacturing Systems With Multiple Unreliable Resources. In IEEE Access, 7: 21006-21019, 2019. doi www
- Improving genetic algorithm using arc consistency technic. In Procedia Computer Science, 159: 1387-1396, 2019. doi www
- Performability modelling and analysis of server virtualised systems subject to workload-dependent software aging. In International Journal of Critical Computer-Based Systems, 9 (3): 248, 2019. doi www
Articles de conférence
- Hapicare: A Healthcare Monitoring System with Self-adaptive Coaching Using Probabilistic Reasoning. In ACS/IEEE International Conference on Computer Systems and Applications - AICCSA 2019, pages 1-8, IEEE, Abu Dhabi, United Arab Emirates, 2019. doi www
- On modelling and evaluation of corrective and preventive maintenance policies of unreliable manufacturing systems. In 2019 6th International Conference on Control, Decision and Information Technologies (CoDIT), pages 1752-1757, IEEE, Paris, France, 2019. doi www
- Performance evaluation of virtual switch with batch arrival using quasi-birth--death process. In 2019 International Conference on Industrial Engineering and Systems Management (IESM), pages 1-6, IEEE, Shanghai, France, 2019. doi www
- Scalable Load Balancing Scheme for Distributed Controllers in Software Defined Data Centers. In 2019 Sixth International Conference on Software Defined Systems (SDS), pages 47-54, IEEE, Rome, Italy, 2019. doi www
- A New Analytical Model for Calculating Elasticity in Cloud Computing. In MSR 2019 - 12ème Colloque sur la Modélisation des Systèmes Réactifs, Angers, France, 2019. www
- Semantic-based collaborative decisional system integrating fuzzy reasoning in an IoT context. In ISD 2019 : 28th International Conference on Information Systems Development, Toulon, France, 2019. www
- WCET of OCaml Bytecode on Microcontrollers: An Automated Method and Its Formalisation. In 19th International Workshop on Worst-Case Execution Time Analysis (WCET 2019), pages 5:1-5:12, Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, Stuttgart, Germany, OpenAccess Series in Informatics (OASIcs) 72, 2019. doi www
- Continuous vs. Discrete Asynchronous Moves: A Certified Approach for Mobile Robots. In 7th International Conference on NETworked sYStems (NETYS 2019), pages 1-15, Marrakech, Morocco, Lecture Notes in Computer Science , 2019. www
- Manuel de savoir-prouver `a l'usage des roboteux et des distributeux. In ALGOTEL 2019 - 21èmes Rencontres Francophones sur les Aspects Algorithmiques des Télécommunications, pages 1-4, Saint Laurent de la Cabrerisse, France, 2019. www
- Urban Traffic Monitoring and Modeling System: An IoT Solution for Enhancing Road Safety. In IINTEC 2019, pages pp. 13-18, Hammamet, Tunisia, 2019. doi www
- Les Protocoles de Déplacement de Robots: l'Algorithmique Distribuée comme Terrain de Jeu pour la Preuve Formelle. In Journées Francophones des Langages Applicatifs, Les Rousses, France, 2019. www
Divers
2018
Articles de revue
- Architectural method to design and control dynamic composite web services. In International Journal of Computer Applications in Technology, 57 (1): 59, 2018. doi www
- Estimating daily evaporation from poorly-monitored lakes using limited meteorological data: A case study within Qaraoun dam - Lebanon. In Journal of Environmental Management, 241: 502-513, 2018. doi www
- IoT-based smart and complex systems: a guest editorial report. In IEEE/CAA Journal of Automatica Sinica, 5 (1): 69-73, 2018. doi www
- Introduction to special issue on verification and evaluation of computer systems. In Innovations in Systems and Software Engineering, 14 (2): 81-82, 2018. doi www
- Delay-dependent partial order reduction technique for real time systems. In Real-Time Systems, 54 (2): 278-306, 2018. doi www
- Performance Analysis of the M/G/c/c+r Queuing System for Cloud Computing Data Centers. In International Journal of Critical Computer-Based Systems, 8 (3-4): 234, 2018. doi www
- Daily river flow prediction based on Two-Phase Constructive Fuzzy Systems Modeling: A case of hydrological -- meteorological measurements asymmetry. In Journal of Hydrology, 558: 255-265, 2018. doi www
Articles de conférence
- Exploiting Local Persistency for Reduced State Space Generation. In 12th International Conference on Verification and Evaluation of Computer and Communication Systems VECoS 2018, pages 166-181, Springer, Porto, Portugal, Verification and Evaluation of Computer and Communication Systems. VECoS 2018. Lecture Notes in Computer Science, vol. 11181 , 2018. doi www
- Liveness Enforcement for a Class of Petri Nets via Resource Allocation. In 2018 IEEE International Conference on Systems, Man, and Cybernetics (SMC), pages 4369-4374, IEEE, Miyazaki, France, 2018. doi www
- Performability evaluation of server virtualized systems under bursty workload. In 14th IFAC Workshop on Discrete Event Systems WODES 2018, IFAC, pages 45-50, Elsevier, Sorrente, Italy, 2018. doi www
- On Persistency in Time Petri Nets. In International Conference on Formal Modeling and Analysis of Timed Systems - FORMATS 2018, pages 108-124, Springer Link, Beijing, China, 2018. doi www
2017
Articles de revue
- Versatile workload-aware power management performability analysis of server virtualized systems. In Journal of Systems and Software, 125: 365-379, 2017. doi www
- Compact Supervisory Control of Discrete Event Systems by Petri Nets With Data Inhibitor Arcs. In IEEE Transactions on Systems, Man, and Cybernetics: Systems, 47 (2): 364-379, 2017. doi www
- Deadlock analysis and control based on Petri nets: A siphon approach review. In Advances in Mechanical Engineering, 9 (5): 168781401769354, 2017. doi www
- Formal verification of complex business processes based on high-level Petri nets. In Information Sciences, 385-386: 39-54, 2017. doi www
- Synthesis of Liveness-Enforcing Petri Net Supervisors Based on a Think-Globally-Act-Locally Approach and Vector Covering for Flexible Manufacturing Systems. In IEEE Access, 5: 16349-16358, 2017. doi www
- On the dependability evaluation of a virtual multiple input multiple output link. In International Journal of Critical Computer-Based Systems, 7 (1): 43, 2017. doi www
Articles de conférence
- Estimating Daily Evaporation from Poorly -- Monitored Lakes using limited Meteorological Data. In SWEDES 12th Conference on Sustainable Develoment of Energy, Water and Environment Systems, Dubrovnik, Croatia, 2017. www
- Mobility Load Balancing over Intra-frequency Heterogeneous Networks Using Handover Adaptation. In International Conference on Verification and Evaluation of Computer and Communication Systems. VECoS 2017, pages 108-123, Montreal, Canada, 2017. doi www
2016
Articles de revue
- A verified abstract machine for functional coroutines. In Electronic Proceedings in Theoretical Computer Science, 212: 1-17, 2016. doi www
- Modeling, implementation and performance analysis of mobility load balancing for LTE downlink data transmission. In International Journal of Computer Networks & Communications, 8 (5), 2016. doi www
Articles de conférence
- Une preuve est une histoire. In Vingt-septièmes Journées Francophones des Langages Applicatifs (JFLA 2016), Saint-Malo, France, 2016. www
2015
Articles de revue
- Guest Editorial for Special Issue Application of Concurrency to System Design. In ACM Transactions on Embedded Computing Systems (TECS), 14 (4): 1-2, 2015. doi www
- On the enforcement of a class of nonlinear constraints on Petri nets. In Automatica, 55: 116-124, 2015. doi www
- Stubborn Sets for Time Petri Nets. In ACM Transactions on Embedded Computing Systems (TECS), 14 (1): 1-25, 2015. doi www
- Necessary and sufficient liveness condition of GS 3 PR Petri nets. In International Journal of Systems Science, 46 (7): 1147-1160, 2015. doi www
2013
Articles de conférence
- A Framework for Verification of SystemC Designs Using SystemC Waiting State Automata. In Integration of Reusable Systems, pages 77-104, San Francisco, United States, 2013. doi www
- Verifying SystemC with predicate abstraction: A component based approach. In 2013 IEEE 14th International Conference on Information Reuse & Integration (IRI), pages 536-545, IEEE, San Francisco, France, 2013. doi www
2012
Articles de conférence
- Vérification Formelle des Processus Workflow Collaboratifs. In Conférence francophone sur les Systèmes Collaboratifs (SysCo12), Paris, France, 2012. www
2010
Articles de revue
- A Tile Logic Based Approach for Software Architecture Description Analysis. In Journal of Software Engineering and Applications, 3 (11): 1067-1079, 2010. doi www
- Probabilistic verification and evaluation of Backoff procedure of the WSN ECo-MAC protocol. In International Journal of Wireless and Mobile Networks, 2010. doi www
- A New Formalism for Modeling a Multi Agent Systems: Agent Petri Nets. In Journal of Software Engineering and Applications, 03 (12): 1118-1124, 2010. doi www
Anciens membres de l'équipe
Projets en cours
- Nom complet: Sûreté et preuve de protocoles: ANR SAPPORO - Financeur: ANR
- Durée: October 2019 - June 2024
- Résumé:
- Nom complet: Nouvelles méthodes informatiques pour les Humanités numériques: HumaNum - Financeur: Laboratoire Cédric
- Durée: January 2021 - December 2021
- Résumé: L’objectif de ce projet exploratoire est d’afficher ces travaux et compétences, actuellement dispersés, sous une étiquette “Humanités numériques”, et de mener un double travail de clarification interne et de communication externe pour identifier le potentiel de cette étiquette comme axe de recherche stable et pérenne. Comment caractériser les problématiques informatiques pertinentes pour participer à une recherche interdisciplinaire équilibrée en humanités numériques ? Le projet exploratoire se place dans une perspective de recherche informatique inspirée par des problématiques SHS. Il s’agit d’identifier ce qui, dans une démarche SHS, suscite une innovation méthodologique en informatique et mène à une recherche véritablement interdisciplinaire, encourageant une réflexion épistémologique croisée (par opposition à la simple mise au point d’outils). Quelles sont les méthodes de l’autre pour produire de la connaissance, comment mes propres méthodes peuvent-elles enrichir celles de l’autre et réciproquement.
- Nom complet: Manuels scolaires inclusifs: MALIN - Financeur: Laboratoire Cédric
- Durée: January 2021 - December 2021
- Résumé: L’école joue un rôle essentiel dans la vie quotidienne des enfants et des adolescents. L’inclusion des enfants en situation de handicap dans les écoles et établissements scolaires ordinaires est un principe posé par la loi du 11 février 2005, pour l’égalité des droits et des chances, la participation et la citoyenneté des personnes handicapées. Ce principe a largement favorisé le nombre d’enfants en situation de handicap inscrits dans leur école de référence (337 395 enfants ont été scolarisés en milieu ordinaire en 2018 alors qu’ils n’étaient que 133 838 en 2004). Malgré ces améliorations quantitatives, la restriction de la participation des enfants en situation de handicap à l’école est indéniable et est à l’origine d’une baisse de leur qualité de vie. Ainsi, la loi du 26 juillet 2019 pour une école de la confiance renforce l’école inclusive et vise à améliorer la qualité de la scolarisation des élèves en situation de handicap. Le service public d’éducation doit dorénavant veiller à l’inclusion scolaire de tous les enfants, sans aucune distinction, et s’assurer que l’environnement est adapté à leur scolarité. Une des difficultés rencontrées par les élèves en situation de handicap est l’inaccessibilité des ressources scolaires qui leur sont proposées en classe. Ainsi, les manuels scolaires sont systématiquement utilisés en France pour accompagner les apprentissages mais ceux-ci ne sont pas accessibles même dans leurs versions numériques. Les avancées technologiques permettent pourtant d’envisager le développement d’interfaces adaptées aux élèves en situation de handicap. Actuellement, ces adaptations et interfaces sont faites manuellement par les adultes qui accompagnent les enfants ou par des organismes de transposition. Même pour un adaptateur expert, le temps d’adaptation d’un manuel entier se compte en centaines d’heures. L’objectif de ce projet est de rendre accessibles les manuels scolaires utilisés dans les classes, aux élèves en situation de handicap en mettant en place des solutions innovantes pour automatiser leur adaptation.
Projets passés
- Nom complet: Systèmes sûrs
- Durée: January 2020 - December 2020
- Résumé:
- Nom complet: Ingénierie des systèmes d'information et de décision
- Durée: January 2020 - December 2020
- Résumé:
- Nom complet: BERGER LEVRAULT
- Durée: April 2017 - May 2018
- Résumé:
- Nom complet: BERGER LEVRAULT 2
- Durée: October 2018 - September 2019
- Résumé: