Team : MoVe - Modeling and Verification

Axes : SSR (👥👥), ASN (👥), TMC (👥).

Team leader :

Tewfik Ziadi Campus Pierre et Marie Curie 25-26/212

Short presentation

MoVe centers its research on the modeling and analysis of complex and dynamic distributed systems. In particular, we put our focus on:

Optimized techniques of formal verification through model-checking.
Development methodologies based on Model-Driven Engineering.
Integration of formal analysis in development processes.
Design and implementation of new programming languages and models to increase the verifiability of distributed programs.

Model engineering, Modeling, Petri nets, Model checking, Program generation, meta-modeling

No event planned at present.

Selected publications

L. Le Frioux, S. Baarir, J. Sopena, F. Kordon : “PaInleSS: a Framework for Parallel SAT Solving.”, The 20^th International Conference on Theory and Applications of Satisfiability Testing, vol. 10491, Lecture Notes in Computer Science, Melbourne, Australia, pp. 233-250, (Springer) [Le Frioux 2017]
L. Hillah, A.‑P. Maesano, F. De Rosa, F. Kordon, P.‑H. Wuillemin, R. Fontanelli, S. Di Bona, D. Guerri, L. Maesano : “Automation and intelligent scheduling of distributed system functional testing: Model-based functional testing in practice”, International Journal on Software Tools for Technology Transfer, vol. 19 (3), pp. 281-308, (Springer Verlag) [Hillah 2017a]
R. Hebig, D. Khelladi, R. Bendraou : “Approaches to Co-Evolution of Metamodels and Models: A Survey”, IEEE Transactions on Software Engineering, vol. 43 (5), pp. 396-414, (Institute of Electrical and Electronics Engineers) [Hebig 2017]
J. Martinez, T. Ziadi, T. Bissyandé, J. Klein, Y. Le Traon : “Bottom-Up Technologies for Reuse: Automated Extractive Adoption of Software Product Lines”, Proceedings of the 39^th International Conference on Software Engineering Companion, Buenos Aires, Argentina, pp. 67-70 [Martinez 2017c]
O. Melekhova, J. Malenfant : “A Token-Based Scheme for Coordinating Decisions in Large-Scale Autonomic Systems”, IEEE 26^th International Conference on Enabling Technologies: Infrastructure for Collaborative Enterprises (WETICE 2017), 2017 IEEE 26^th International Conference on Enabling Technologies: Infrastructure for Collaborative Enterprises (WETICE), Poznan, Poland, (IEEE Computer Society) [Melekhova 2017]
E. Renault, A. Duret‑Lutz, F. Kordon, D. Poitrenaud : “Variations on Parallel Explicit Emptiness Checks for Generalized Büchi Automata”, International Journal on Software Tools for Technology Transfer, vol. 19 (6), pp. 653-673, (Springer Verlag) [Renault 2017]
B. Bérard, P. Lafourcade, L. Millet, M. Potop‑Butucaru, Y. Thierry‑Mieg, S. Tixeuil : “Formal verification of mobile robot protocols”, Distributed Computing, vol. 29 (6), pp. 459-487, (Springer Verlag) [Bérard 2016c]
B. Bérard, S. Haddad, A. Jovanovic, D. Lime : “Interrupt Timed Automata with Auxiliary Clocks and Parameters”, Fundamenta Informaticae, vol. 143 (3-4), pp. 235-259, (Polskie Towarzystwo Matematyczne) [Bérard 2016d]
B. Bérard, O. Kouchnarenko, J. Mullins, M. Sassolas : “Preserving opacity on Interval Markov Chains under simulation”, Proceedings of 13^th International Workshop on Discrete Event Systems (WODES) 2016, IEEE, Xi'an, China, pp. 319-324 [Bérard 2016b]
F. Kordon, H. Garavel, L. Hillah, E. Paviot‑Adet, L. Jezequel, C. Rodríguez, F. Hulin‑Hubard : “MCC’2015 – The Fifth Model Checking Contest”, LNCS Transactions on Petri Nets and Other Models of Concurrency, vol. 9930, Lecture Notes in Computer Science, pp. 262-273, (Springer) [Kordon 2016b]
L. Hillah, A.‑P. Maesano, L. Maesano, F. De Rosa, F. Kordon, P.‑H. Wuillemin : “Service functional testing automation with intelligent scheduling and planning”, Symposium on Applied Computing (SAC), Proceeding of the 31^st Annual ACM Symposium on Applied Computing, Pisa, Italy, pp. 1605-1610 [Hillah 2016]
D. Khelladi, R. Hebig, R. Bendraou, J. Robin, M.‑P. Gervais : “Detecting complex changes and refactorings during (Meta)model evolution”, Information Systems, vol. 62, Information Systems, (Elsevier) [Khelladi 2016e]
M. Güdemann, P. Poizat, G. Salaün, L. Ye : “VerChor: A Framework for the Design and Verification of Choreographies”, IEEE Transactions on Services Computing, vol. 9 (4), pp. 647-660, (IEEE) [Güdemann 2016]
Th. Brihaye, M. Estiévenart, G. Geeraerts, H.‑M. Ho, B. Monmege, N. Sznajder : “Real-time Synthesis is Hard!”, Proceedings of the 14^th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS'16), vol. 9884, Lecture Notes in Computer Science, Québec City, Canada, pp. 105-120, (Springer) [Brihaye 2016]
Ah. Chaouche, A. El Fallah‑Seghrouchni, J.‑M. Ilié, D. Saidouni : “Smart Agent Foundations: From Planning to Spatio-temporal Guidance”, chapter in Enablers for Smart Cities, pp. 33-63, (John Wiley & Sons, Inc), (ISBN: 9781848219588) [Chaouche 2016b]
F. Kordon, D. Moldt : “Application and Theory of Petri Nets and Concurrency: 37th International Conference, PETRI NETS 2016, Toruń, Poland, June 19-24, 2016. Proceedings”, vol. 9695, Lecture Notes in Computer Science, Torun, Poland, (ISBN: 978-3-319-39085-7) [Kordon 2016a]
E. Renault, A. Duret‑Lutz, F. Kordon, D. Poitrenaud : “Parallel Explicit Model Checking for Generalized Büchi Automata”, 21^th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2015, vol. 9035, Lecture Notes in Computer Science, London, United Kingdom, pp. 613-627, (Springer) [Renault 2015]
S. Lamprier, N. Baskiotis, T. Ziadi, L. Hillah : “The CARE Platform for the Analysis of Behavior Model Inference Techniques”, Information and Software Technology, vol. 60, pp. 32-50, (Elsevier) [Lamprier 2015a]
J. Martinez, T. Ziadi, Tegawendé F. Bissyandé, J. Klein, Y. Le Traon : “Automating the Extraction of Model-Based Software Product Lines from Model Variants”, ASE 2015 - 30^th IEEE/ACM International Conference on Automated Software Engineering, Lincoln, Nebraska, United States, pp. 396-406, (IEEE) [Martinez 2015d]
B. Bérard, K. Chatterjee, N. Sznajder : “Probabilistic Opacity for Markov Decision Processes”, Information Processing Letters, vol. 115 (1), pp. 52-59, (Elsevier) [Bérard 2015b]
A. Ben Salem, A. Duret‑Lutz, F. Kordon, Y. Thierry‑Mieg : “Symbolic Model Checking of stutter invariant properties Using Generalized Testing Automata”, 20^th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2014, vol. 8413, Lecture Notes in Computer Science, Grenoble, France, pp. 440-454, (Springer) [Ben Salem 2014]
J.‑R. Falleri, X. Blanc, R. Bendraou, M. Almeida Da Silva, C. Teyton : “Incremental inconsistency detection with low memory overhead”, Software: Practice and Experience, vol. 44 (5), pp. 621-641, (Wiley) [Falleri 2014]
Y. Laurent, R. Bendraou, S. Baarir, M.‑P. Gervais : “Formalization of fUML: An Application to Process Verification”, CAiSE 2014 - The 26^th International Conference on Advanced Information Systems Engineering, vol. 8484, Lecture Notes in Computer Science, Thessaloniki, Greece, pp. 347-363, (Springer) [Laurent 2014b]
L. Millet, M. Potop‑Butucaru, N. Sznajder, S. Tixeuil : “On the Synthesis of Mobile Robots Algorithms: the Case of Ring Gathering”, SSS 2014 - 16^th International Symposium on Stabilization, Safety and Security of Distributed Systems, vol. 8756, Lecture Notes in Computer Science, Paderborn, Germany, pp. 237-251, (Springer) [Millet 2014]
A. Yessad, I. Mounier, J.‑M. Labat, F. Kordon, Th. Carron : “Have you found the error? A Formal Framework for Learning Game Verification”, 9^th European Conference on Technology Enhanced Learning, vol. 8719, Lecture Notes in Computer Science, Graz, Austria, pp. 476-481, (Springer) [Yessad 2014a]
M. Colange, S. Baarir, F. Kordon, Y. Thierry‑Mieg : “Towards Distributed Software Model-Checking using Decision Diagrams”, 25^th International Conference on Computer Aided Verification (CAV), vol. 8044, Lecture Notes in Computer Science, Saint-Petersbourg, Russian Federation, pp. 830-845, (Springer Verlag) [Colange 2013]
S. Lamprier, N. Baskiotis, T. Ziadi, L. Hillah : “CARE: a platform for reliable Comparison and Analysis of Reverse-Engineering techniques”, 18^th IEEE International Conference on Engineering of Complex Computer Systems -- ICECCS, Singapore, Singapore, pp. 252-255, (IEEE) [Lamprier 2013]
H. Nguyen, P. Poizat, F. Zaïdi : “Automatic Skeleton Generation for Data-Aware Service Choreographies”, 24^th IEEE International Symposium on Software Reliability Engineering, ISSRE 2013, Pasadena, CA, United States, pp. 320-329, (IEEE) [Nguyen 2013]
R. Khefifi, P. Poizat, F. Saïs : “Automatic Composition of Form-Based Services in a Context-Aware Personal Information Space”, 11^th International Conference on Service Oriented Computing, ICSOC 2013, vol. 8274, Lecture Notes in Computer Science, Berlin, Germany, pp. 575-583, (Springer) [Khefifi 2013a]
P. Gastin, N. Sznajder : “Fair Synthesis for Asynchronous Distributed Systems”, ACM Transactions on Computational Logic, vol. 14 (2), pp. 9, (Association for Computing Machinery) [Gastin 2013]
M. Jaume, R. Andriatsimandefitra, V. Viet Triem Tong, L. Mé : “Secure states versus Secure executions: From access control to flow control”, ICISS 2013 - 9^th International Conference on Information Systems Security, vol. 8303, Lecture Notes in Computer Science, Calcutta, India, pp. 148-162, (Springer) [Jaume 2013]
B. Bérard, S. Haddad, M. Sassolas, N. Sznajder : “Concurrent Games on VASS with Inhibition”, 23rd International Conference on Concurrency Theory (CONCUR'12), vol. 7454, Lecture Notes in Computer Science, Newcastle upon Tyne, United Kingdom, pp. 39-52, (Springer) [Bérard 2012b]
T. Ziadi, L. Frias, M. Almeida Da Silva, M. Ziane : “Feature Identification from the Source Code of Product Variants”, 16^th European Conference on Software Maintenance and Reengineering (CSMR), Szeged, Hungary, pp. 417-422, (IEEE Computer Science) [Ziadi 2012]

All…