Publications et productions scientifiques


Journaux

  1. Kais Klai, Samir Tata and Hanen Ochi. Generic and Specific Compatibility Criteria for Web Service Compatibility: Formal Abstraction and Modular Verification. International Journal of Web Services Research 9(4) 45-68, 2012.

  2. Christine Choppy, Anna Dedova, Sami Evangelista, Kais Klai, Laure Petrucci and Samir Youcef. Modelling and Formal Verification of the NEO Protocol. In Transactions on Petri Nets and Other Models of Concurrency, TOPNOC, pp 197-225, 2012.

  3. Etienne André, Christine Choppy et Kais Klai. Formalizing non-concurrent UML State Machines Using Colored Petri Nets. ACM SIGSOFT Software Engineering Notes, pp 1-8, Volume 37, n° 1, 2012.

  4. Kais Klai, Samir Tata and Jörg Desel. Symbolic Abstraction and Deadlock Freeness Verification of Inter-Enterprise Processes. In Data & Knowledge Engineering (D&KE), pp 467-482, volume 70, n°5, 2011.

  5. Christine Choppy, Kais Klai and Hacene Zidani. Formal Verification of UML State Diagrams: a Petri net based approach. ACM SIGSOFT Software Engineering Notes, pp 1-8, Volume 36, n° 1, 2011.

  6. Samir Tata, Kais Klai and Noaman Ould Ahmed M'bareck. CoopFlow: A Bottom-Up Approach to Workflow Cooperation for Short-Term Virtual Enterprises. In IEEE Transactions on Services Computing (TSC). Volume 1, Issue 4. pp 214-228, Oct-Dec. 2008.

Conférences internationales

  1. Kais Klai, Naim Aber and Laure Petrucci. A New Approach To Abstract Reachability State Space of Time Petri Nets. In 20th International Symposium on Temporal Representation and Reasoning TIME’13, .

  2. Mourad Amziani, Kais Klai, Tarek Melliti and Samir Tata Time-based Evaluation of Service-based Business Process Elasticity in the Cloud, The 5th IEEE International Conference on Cloud Computing Technology and Science (CloudCom 2013), December 2-5, 2013, Bristol, United Kingdom.

  3. Kais Klai and Samir Tata. Formal Modeling of Elastic Service-based Business Processes. In 10th International Conference on Services Computiong, IEEE SCC 3013.

  4. Kais Klai, Hanen Ochi and Samir Tata. Formal Abstraction and Compatibility Checking of Web Services. In 20th International Conference on Web Services, IEEE ICWS, 163-170, 2013.

  5. Kais Klai and Hanen Ochi. Checking Compatibility of Web Services Behaviorally. Fondamentals of Software Engineering FSEN 2013, Lecture Notes in Computer Science, Springer-Verlag, 267-282, 2013.

  6. Kais Klai et Jörg Desel. Checking Soundness of Business Processes Using Symbolic Observation Graphs. In Proceedings of FMOODS/FORTE. Lecture Notes in Computer Science pp 67-83, Springer-Verlag, 2012.

  7. Leila Abidi, Christophe Cérin et Kais Klai. Design, Verification and Prototyping the Next Generation of Desktop Grid Middleware. In Proceedings of GPC. Lecture Notes in Computer Science pp 74-88, Springer-Verlag, volume 7296, 2012.

  8. Kais Klai and Hanen Ochi. Checking Compatibility of Web Services Using SOGs. In Proceedings 2012 IEEE 19th International Conference on Web Services, pp 670-671, Honolulu, HI, USA, June 24-29, 2012.

  9. Kais Klai and Hanen Ochi. Modular verification of inter-enterprise Business Processes. In The IEEE Fourth International Conference on Information, Process, and Knowledge Management, eKNOW 2012, pp- 155-161, January 30 - February 4, 2012 - Valencia, Spain.

  10. Alexandre Duret-Lutz, Kais Klai, Denis Poitrenaud et Yann Thierry-Mieg. Self-Loop Aggregation Product - A New Hybrid Approach to On-the-Fly LTL Model Checking. In Proceedings of 9th International Symposium on Automated Technology for Verification and Analysis, Taipei, Taiwan. Lecture Notes in Computer Science pp 336-350, Springer-Verlag, 2011.

  11. Christine Choppy, Anna Dedova, Sami Evangelista, Silien Hong, Kais Klai and Laure Petrucci. The NEO Protocol for Large-Scale Distributed Database Systems: Modelling and Initial Verification. In Proceedings of International Conference of Application and Theory of Petri nets (ICATPN 2010), volume 16128 LNCS, pp. 145-164, Springer-Verlag, June 21-25 2010.

  12. K. Klai, S. Tata and J. Desel. Symbolic Abstraction and Deadlock Freeness Verification of Inter-Enterprise Processes. In Proceedings of the 29th International Conference On Business Process Management (BPM 2009), Ulm, Germany. Lecture Notes in Computer Science, Springer-Verlag, September 8-10 2009.

  13. K. Klai and D. Poitrenaud. MC-SOG: An LTL Model Checker Based on Symbolic Observation Graphs. In Petri Nets, Proceedings of the 29th International Conference On Application and Theory of Petri Nets (ICATPN 2008), Xi'an China, Lecture Notes in Computer Science, Springer-Verlag, June 23-27 2008.

  14. K. Klai and L. Petrucci. Modular Construction of the Symbolic Observation Graph. In Proc. the 8th International Conference on Application of concurrency to System Design (ACSD 2008), The Institute of Computing Theory and Technology at Xidian University, Xi'an, China, June 23-27, 2008.

  15. K. Klai, L. Petrucci and M. Reniers. An Incremental and Modular Technique for Checking LTL\X Properties of Petri Nets. In Proc. 27th International Conference on Formal Methods for Networked and Distributed Systems (FORTE'07), Tallinn, Estonia, Lecture Notes in Computer Science. pp. 280-295 Springer-Verlag, 2007.

  16. K. Klai, N. O. A. M’bareck and S. Tata, A behavioural technique for workflow abstraction and matching. In Proc. 4th International Conference on Business Process Management (BPM 2006), Vienna, Austria, Volume 4102 of Lecture Notes in Computer Science. pp. 477- 483 Springer-Verlag, 2006.

  17. K. Klai, S. Haddad and Jean-Michel Ilié. Modular Verification of Petri nets properties: a Structure-based Approach. In Proceedings of the 25th IFIP WG 6.1 International Conference on Formal Techniques for Networked and Distributed Systems (FORTE 2005), National Taiwan University, volume 3731 of Lecture Notes in Computer Science, pp. 189--203, Springer-Verlag, October 2-5 2005.

  18. K. Barkaoui, J-M. Couvreur and K. Klai. On the Equivalence between Liveness and Deadlock-Freeness. In Petri Nets, Proceedings of the 26th International Conference On Application and Theory of Petri Nets (ICATPN 2005), Miami, Florida USA, volume 3536 of Lecture Notes in Computer Science, pp. 90—107, Springer-Verlag, June 20-25 2005.

  19. S. Haddad, J-M. Ilié et K. Klai. Design and Evaluation of a Symbolic and Abstraction based model checker. In Proceeding of 2sd International Symposium on Automated Technology for Verification and Analysis (ATVA'04), National Taiwan University, volume 3299 of Lecture Notes in Computer Science, pp. 196—210, October 31 - November 03 2004.

  20. S. Haddad, J-M. Ilié et K. Klai. Symbolic Observation Graph: An efficient structure for on-the-fly linear time model checker. In The 15th IEEE International Symposium on Software Reliability Engineering (ISSRE’04), Saint-Malo, Bretagne, France 2004.

  21. J-M. Ilié, K. Klai et Z. Belhassen. A Modular Verification Methodology for D-NRI Petri Nets. ACS/IEEE International Conference on Computer Systems and Applications (AICCSA'03), July 2003, Tunis, Tunisia.

  22. S. Haddad, J-M. Ilié et K. Klai. An Incremental Verification Technique Using Decomposition of Petri Nets. In IEEE International Conference on Systems, Man and Cybernetics (SMC 02), Hammamet Tunisia 2002.

Workshops internationaux

  1. Kais Klai, Naim Aber and Laure Petrucci. Verification of Reachability Properties for Time Petri Nets. 7th International Workshop on Reachability Problem RP’13.

  2. Etienne André, Kais Klai, Hanen Ochi et Laure Petrucci. A Counterexample-Based Incremental and Modular Verification Approach. Large-Scale Complex IT Systems. Development, Operation and Management - 17th Monterey Workshop, Oxford, UK, March 19-21, 2012, Revised Selected Papers. Lecture Notes in Computer Science, Springer volume, 2012

  3. Kais Klai and Walid Gaaloul. Petri Net Modeling and Verification of Transactional Workflows. In Proceedings of 20th IEEE International Workshops on Enabling Technologies : Infrastructures for Collaborative Enterprises, WETICE 2011, pp 176-184, Paris, France, 27-29 June 2011.

  4. O. Bertrand, A. Calonne, C. Choppy, S. Hong, K. Klai, F. Kordon, Y. Okuji, E. Paviot-Adet, L. Petrucci, and J.-P. Smets. Verification of large-scale distributed database systems in the NEOPPOD project. In Proceedings Workshop on Petri Nets and Software Engineering (PNSE’09, associated with Petri Nets 2009), Paris, France , pages 315–316, June 2009.

  5. Kais Klai and Laure Petrucci. Modular Construction of the Symbolic Observation Graph. In Proceedings 1st International Workshop on Verification and Evaluation of Computer and Communication Systems (VECOS'07), pp 6, may 2007, Algiers, Algeria, British Computer Society, eWiC, 2007.

  6. Kais Klai, Samir Tata and Issam Chebbi, An observation-based algorithm for workflow matching. In The Fourth International Workshop on Modelling, Simulation, Verification and Validation of Enterprise Information Systems (MSVVEIS 2006), Paphos Ciprus, Mai 2006.

  7. Kais Klai and Samir Tata. Abstraction-based Workflow Cooperation Using Petri Net Theory. In 3rd International Workshop on Distributed and Mobile Cooperation (DMC 2005), Linkoping University, Sweden.

Rapports techniques

      1. Alexandre Duret-Lutz, Kais Klai, Denis Poitrenaud et Yann Thierry-Mieg. Combining Explicit and Symbolic Approaches for Better On-the-Fly LTL Model Checking. CoRR 2011.

Conférences nationales

        1. Kais Klai, Samir Tata and Issam Chebbi. Workflow interconnection using symbolic observation graph. In INFORSID 2006 (Systèmes d’information et services web), june 2006, Hammamet Tunisia.

        2. J-M. Ilié and K. Klai. A Modular Verification Methodology for D-NRI Petri Nets. MOVEP (Modelling and Verification of Parallel Processes), Nantes, Juillet 2000.

Outils

Hamez, L. Hillah, K. Klai, F. Kordon, L. Petrucci, D. Poitrenaud, and Y. Thierry-Mieg. CoSyVerif : Complex Systems Verification. Tool presentation at PetriNets’08, June 2008.