Secure systems

The “Secure Systems” team focuses on specification, design, verification and evaluation of systems, in particular safety and security of critical applications. The objective is to develop methods, techniques and tools allowing to express properties of applications and to demonstrate that these applications satisfy the expected specification. All our research falls within the general framework of formal methods and is structured around three axis : “Typing, Semantics and Proofs”, “Software Architecture and System Architecture and Product Lines” and “Verification and Evaluation of Parallel and Asynchronous Systems”.

Publications

2021

Articles de revue

  1. Wang, S.; Duo, W.; Guo, X.; Jiang, X.; You, D.; Barkaoui, K. and Zhou, M. 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 

2020

Articles de revue

  1. Barkaoui, K. and Boucheneb, H. Exploiting local persistency for reduced state-space generation. In Innovations in Systems and Software Engineering, 16 (2): 181-197, 2020. doi  www 
  1. Jabbar, R.; Kharbeche, M.; al-Khalifa, K.; Krichen, M. and Barkaoui, K. Blockchain for the Internet of Vehicles: A Decentralized IoT Solution for Vehicles Communication Using Ethereum. In Sensors, 20 (14): 3928, 2020. doi  www 
  1. Barkaoui, K.; Boucheneb, H. and Li, Z. Exploiting local persistency for reduced state-space generation. In Innovations in Systems and Software Engineering, 2020. doi  www 
  1. Lakaour, L.; Aissani, D.; Adel-Aissanou, K.; Barkaoui, K. and Ziani, S. An unreliable single server retrial queue with collisions and transmission errors. In Communications in Statistics - Theory and Methods: 1-25, 2020. doi  www 

Chapitres d'ouvrage

  1. Kordestani, H.; Barkaoui, K. and Zahran, W. HapiFabric: A Teleconsultation Framework Based on Hyperledger Fabric. In HapiFabric: A Teleconsultation Framework Based on Hyperledger Fabric. In: Themistocleous M., Papadaki M., Kamal M.M. (eds) Information Systems. EMCIS 2020. Lecture Notes in Business Information Processing, vol 402. Springer, Cham., pages 399-414, 2020. doi  www 

Articles de conférence

  1. Jabbar, R.; Fetais, N.; Krichen, M. and Barkaoui, K. 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 
  1. Kordestani, H.; Barkaoui, K. and Zahran, W. 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 
  1. Jabbar, R.; Krichen, M.; Shinoy, M.; Kharbeche, M.; Fetais, N. and Barkaoui, K. 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 
  1. Jabbar, R.; Shinoy, M.; Kharbeche, M.; al-Khalifa, K.; Krichen, M. and Barkaoui, K. 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 
  1. Jabbar, R.; Krichen, M.; Kharbeche, M.; Fetais, N. and Barkaoui, K. 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, France, 2020. doi  www 
  1. Jabbar, R.; Krichen, M.; Fetais, N. and Barkaoui, K. 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 
  1. Balabonski, T.; Courtieu, P.; Pelle, R.; Rieg, L.; Tixeuil, S. and Urbain, X. 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 

Non publié

  1. Jabbar, R.; Krichen, M.; Kharbeche, M.; Fetais, N. and Barkaoui, K. 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 
  1. Jabbar, R.; Krichen, M.; Kharbeche, M.; Fetais, N. and Barkaoui, K. A Model-Based Testing Framework for Validating an IoT Solution for Blockchain-Based Vehicles Communication. , working paper or preprint. www 
  1. Jabbar, R.; Krichen, M.; Fetais, N. and Barkaoui, K. Formal Verification and Model-Based Testing Techniques for Validating a Blockchain-Based Healthcare Records Sharing System. , working paper or preprint. www 
  1. Jabbar, R.; Krichen, M.; Fetais, N. and Barkaoui, K. 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 

2019

Articles de revue

  1. Dou, H.; Barkaoui, K.; Boucheneb, H.; Jiang, X. and Wang, S. Maximal Good Step Graph Methods for Reducing the Generation of the State Space. In IEEE Access, 7: 155805-155817, 2019. doi  www 
  1. Zouita, M.; Bouamama, S. and Barkaoui, K. Improving genetic algorithm using arc consistency technic. In Procedia Computer Science, 159: 1387-1396, 2019. doi  www 
  1. Lakaour, L.; Aissani, D.; Adel-Aissanou, K. and Barkaoui, K. M/M/1 Retrial Queue with Collisions and Transmission Errors. In Methodology and Computing in Applied Probability, 21 (4): 1395-1406, 2019. doi  www 
  1. Dou, H.; Barkaoui, K.; Boucheneb, H.; Jiang, X. and Wang, S. Maximal Good Step Graph Methods for Reducing the Generation of the State Space. In IEEE Access, 7: 155805-155817, 2019. doi  www 
  1. Li, X.; Liu, G.; Li, Z.; Wu, N. and Barkaoui, K. Elementary Siphon-Based Robust Control for Automated Manufacturing Systems With Multiple Unreliable Resources. In IEEE Access, 7: 21006-21019, 2019. doi  www 
  1. Escheikh, M.; Tayachi, Z. and Barkaoui, K. 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

  1. Varoumas, S. and Crolard, T. 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 
  1. Tayachi, Z.; Escheikh, M. and Barkaoui, K. 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 
  1. Kordestani, H.; Mojarad, R.; Chibani, A.; Osmani, A.; AMIRAT, Y.; Barkaoui, K. and Zahran, W. Hapicare: A Healthcare Monitoring System with Self-Adaptive Coaching using Probabilistic Reasoning. In 2019 IEEE/ACS 16th International Conference on Computer Systems and Applications (AICCSA), pages 1-8, IEEE, Abu Dhabi, France, 2019. doi  www 
  1. Kordestani, H.; Mojarad, R.; Chibani, A.; Osmani, A.; AMIRAT, Y.; Barkaoui, K. and Zahran, W. 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 
  1. Barkaoui, K.; Outamazirt, A. and Aissani, d. 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 
  1. Escheikh, M. and Barkaoui, K. 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 
  1. Tayachi, Z.; Escheikh, M. and Barkaoui, K. 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 
  1. Besbes, G.; Baazaoui-Zghal, H. and Pollet, Y. 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 
  1. Meriah, R.; Barkaoui, K.; Liu, G. and Driss, O. B. 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 
  1. Balabonski, T.; Courtieu, P.; Pelle, R.; Rieg, L.; Tixeuil, S. and Urbain, X. 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 
  1. Balabonski, T.; Courtieu, P.; Pelle, R.; Rieg, L.; Tixeuil, S. and Urbain, X. 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 

Divers

  1. Dantan, J.; Zghal, H. B.; Pollet, Y. and Dronga, F. Environnement d'aide `a la décision pour l'agriculture numérique. , Poster. doi  www 

2018

Articles de revue

  1. Wu, N.; Li, Z.; Barkaoui, K.; Li, X.; Murata, T. and Zhou, M. IoT-based smart and complex systems: a guest editorial report. In IEEE/CAA Journal of Automatica Sinica, 5 (1): 69-73, 2018. doi  www 
  1. Barkaoui, K. and Boucheneb, H. 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 
  1. Bou-Fakhreddine, B.; MOUGHARBEL, I.; Faye, A. and Pollet, Y. 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 
  1. Boucheneb, H. and Barkaoui, K. Delay-dependent partial order reduction technique for real time systems. In Real-Time Systems, 54 (2): 278-306, 2018. doi  www 
  1. Djenouhat, M. A.; BELALA, F. and Barkaoui, K. Architectural method to design and control dynamic composite web services. In International Journal of Computer Applications in Technology, 57 (1): 59, 2018. doi  www 
  1. Bou-Fakhreddine, B.; MOUGHARBEL, I.; Faye, A.; Abou Chakra, S. and Pollet, Y. 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 
  1. Outamazirt, A.; Escheikh, M.; Aissani, D.; Barkaoui, K. and Lekadir, O. 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 

Articles de conférence

  1. Barkaoui, K.; Boucheneb, H. and Li, Z. 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 
  1. Barkaoui, K. and Boucheneb, H. 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 
  1. You, D.; Wang, S.; Dou, H.; Duo, W.; Barkaoui, K. and Seatzu, C. 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 
  1. Escheikh, M.; Tayachi, Z. and Barkaoui, K. 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 

2017

Articles de revue

  1. Hou, Y. and Barkaoui, K. Deadlock analysis and control based on Petri nets: A siphon approach review. In Advances in Mechanical Engineering, 9 (5): 168781401769354, 2017. doi  www 
  1. Kheldoun, A.; Barkaoui, K. and Ioualalen, M. Formal verification of complex business processes based on high-level Petri nets. In Information Sciences, 385-386: 39-54, 2017. doi  www 
  1. Li, C.; Chen, Y.; Li, Z. and Barkaoui, K. 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 
  1. Escheikh, M.; Barkaoui, K. and Jouini, H. Versatile workload-aware power management performability analysis of server virtualized systems. In Journal of Systems and Software, 125: 365-379, 2017. doi  www 
  1. Chen, Y.; Li, Z.; Barkaoui, K.; Wu, N. and Zhou, M. 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 
  1. Escheikh, M. and Barkaoui, K. 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

  1. Bou-Fakhreddine, B.; Abou-Chakra, S.; MOUGHARBEL, I.; Alain, F. and Pollet, Y. 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 
  1. Jouini, H.; Escheikh, M.; Barkaoui, K. and Ezzedine, T. 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

  1. Crolard, T. A verified abstract machine for functional coroutines. In Electronic Proceedings in Theoretical Computer Science, 212: 1-17, 2016. doi  www 
  1. Escheikh, M.; Jouini, H. and Barkaoui, K. 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

  1. Bosser, A-G.; Aponte, M-V.; Courtieu, P. and Forest, J. 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

  1. Chen, Y.; Li, Z.; Barkaoui, K. and Giua, A. On the enforcement of a class of nonlinear constraints on Petri nets. In Automatica, 55: 116-124, 2015. doi  www 
  1. Barkaoui, K.; Bernardinello, L. and Mokhov, A. 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 
  1. Boucheneb, H. and Barkaoui, K. Stubborn Sets for Time Petri Nets. In ACM Transactions on Embedded Computing Systems (TECS), 14 (1): 1-25, 2015. doi  www 
  1. Liu, G. and Barkaoui, K. 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

  1. Harrath, N.; Monsuez, B. and Barkaoui, K. 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 
  1. Harrath, N.; Monsuez, B. and Barkaoui, K. 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

  1. Sbai, Z. and Barkaoui, K. 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

  1. Choutri, A.; Belala, F. and Barkaoui, K. A Tile Logic Based Approach for Software Architecture Description Analysis. In Journal of Software Engineering and Applications, 3 (11): 1067-1079, 2010. doi  www 
  1. Zayani, H.; Barkaoui, K. and Ayed, R. B. Probabilistic verification and evaluation of Backoff procedure of the WSN ECo-MAC protocol. In International Journal of Wireless and Mobile Networks, 2010. doi  www 
  1. Marzougui, B.; Hassine, K. and Barkaoui, K. 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 

Projects of team

Ongoing projects

    Past projects

      Top