Équipe : MoVe - Modélisation et Vérification

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

Co-Responsables :

Jean-François Pradat-Peyre Campus Pierre et Marie Curie 25-26/215
Yann Thierry-Mieg Campus Pierre et Marie Curie 25-26/210

Aucune manisfestation prévue actuellement.

Brève présentation

L'équipe MoVe centre ses recherches sur la modélisation et l'analyse de systèmes répartis complexes et dynamiques. En particulier, nous nous focalisons sur les aspects suivants :

Techniques optimisées de vérification formelle par model checking,
Méthodologies de développement basées sur l'ingénierie dirigée par les modèles,
Intégration de l'analyse formelle dans les processus de développement,
Conception et implantation de nouveaux langages et modèles de programmation pour accroître la vérifiabilité de programmes répartis.

Ingénierie des modèles, Modélisation, Réseaux de Petri, Model Checking, Génération de programme, Meta-modélisation

Sélection de publications

B. Barbot, B. Bérard, Y. Duplouy, S. Haddad : “Integrating Simulink Models into the Model Checker Cosmos” Application and Theory of Petri Nets and Concurrency - Petri Nets 2018, vol. 10877, Lecture Notes in Computer Sciences, Bratislava, Slovakia, pp. 363-373, (Springer)[Barbot 2018b]
R. Bendraou, B. Combemale, X. Crégut, M.‑P. Gervais : “Definition of an eXecutable SPEM 2.0” 14^th Asia-Pacific Software Engineering Conference (APSEC), Nagoya, Japan, pp. 390-397, (IEEE Computer Society)[Bendraou 2007a]
B. Bérard, B. Bollig, P. Bouyer, M. Függer, N. Sznajder : “Synthesis in presence of dynamic links” Information and Computation, vol. 289 (Part B), pp. 104856, (Elsevier)[Bérard 2022a]
B. Bérard, P. Bouyer, V. Jugé : “Finite Bisimulations for Dynamical Systems with Overlapping Trajectories” LIPICS, vol. 119, Birmingham, United Kingdom, pp. 26:1-26:17, (Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik)[Bérard 2018b]
B. Bérard, S. Haar, L. Hélouët : “Hyper Partial Order Logic” 38^th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2018, vol. 122, Leibniz International Proceedings in Informatics (LIPIcs), Ahmedabad, India, pp. 20:1-20:21, (Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik)[Bérard 2018c]
B. Bérard, S. Haar, S. Schmitz, S. Schwoon : “The Complexity of Diagnosability and Opacity Verification for Petri Nets” Fundamenta Informaticae, vol. 161 (4), pp. 317-349, (Polskie Towarzystwo Matematyczne)[Bérard 2018d]
B. Bérard, S. Haddad : “Revisiting Reachability in Polynomial Interrupt Timed Automata” Information Processing Letters, vol. 174, pp. 106208, (Elsevier)[Bérard 2022b]
B. Bérard, S. Haddad, E. Lefaucheux : “Probabilistic Disclosure: Maximisation vs. Minimisation” FSTTCS 2017, Kanpur, India, pp. 13:1-13:14[Bérard 2017c]
B. Bérard, S. Haddad, C. Picaronny, M. Safey El Din, M. Sassolas : “Polynomial interrupt timed automata: Verification and expressiveness” Information and Computation, vol. 277, pp. 104580, (Elsevier)[Bérard 2021]
B. Bérard, L. Hélouët, J. Mullins : “Non-interference in partial order models” ACM Transactions on Embedded Computing Systems (TECS), vol. 16 (2), Application and Theory of Petri Nets and Other Models of Concurrency: Special Issue of Selected Papers from Petri Nets 2015, pp. 44:1-44:34, (ACM)[Bérard 2017a]
B. Bérard, O. Kouchnarenko, J. Mullins, M. Sassolas : “Opacity for linear constraint Markov chains” Discrete Event Dynamic Systems, vol. 28 (1), pp. 83-108, (Springer Verlag)[Bérard 2018a]
B. Bollig, M. Lehaut, N. Sznajder : “Round-Bounded Control of Parameterized Systems” 16^th International Symposium on Automated Technology for Verification and Analysis (ATVA 2018), vol. 11138, Proceedings of the 16^th International Symposium on Automated Technology for Verification and Analysis (ATVA 2018), Los Angeles, California, United States, pp. 370-386, (Springer)[Bollig 2018]
Th. Bui, N. Papoulias, S. Stinckwich, M. Ziane, B. Roche : “The Kendrick modelling platform: language abstractions and tools for epidemiology” BMC Bioinformatics, vol. 20 (1), pp. 312, (BioMed Central)[Bui 2019]
Ah. Chaouche, J.‑M. Ilié, F. Pêcheux : “Dealing with Failures for Execution Consistency in Context-aware Systems” Procedia Computer Science, vol. 177, pp. 212-219, (Elsevier)[Chaouche 2020]
A. Chueshev, J. Lawall, R. Bendraou, T. Ziadi : “Expanding the Number of Reviewers in Open-Source Projects by Recommending Appropriate Developers” ICSME 2020 - International Conference on Software Maintenance and Evolution, Adélaïde / Virtual, Australia[Chueshev 2020]
S. Grüner, A. Burger, H. Abukwaik, S. El‑Sharkawy, K. Schmid, T. Ziadi, A. Paule, F. Suda, A. Viehl : “Demonstration of a Toolchain for Feature Extraction, Analysis and Visualization on an Industrial Case Study” 2019 IEEE 17^th International Conference on Industrial Informatics (INDIN), Helsinki, Finland, pp. 459-465, (IEEE)[Grüner 2019]
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]
S. Houhou, S. Baarir, P. Poizat, Ph. Quéinnec : “A First-Order Logic Semantics for Communication-Parametric BPMN Collaborations” BPM 2019: Business Process Management, vol. 11675, Lecture Notes in Computer Science book series (LNCS), Vienna, Austria, pp. 52-68[Houhou 2019]
S. Houhou, S. Baarir, P. Poizat, Ph. Quéinnec : “A Direct Formal Semantics for BPMN Time-Related Constructs” ENASE 2021 - 16^th International Conference on Evaluation of Novel Approaches to Software Engineering, online, Czechia, pp. 138-149[Houhou 2021]
S. Houhou, S. Baarir, P. Poizat, Ph. Quéinnec, L. Kahloud : “A First-Order Logic Verification Framework for Communication-Parametric and Time-Aware BPMN Collaborations” Information Systems, vol. 104, pp. 101765, (Elsevier)[Houhou 2022]
J.‑M. Ilié, Ah. Chaouche, F. Pêcheux : “A Reinforcement Learning Integrating Distributed Caches for Contextual Road Navigation” International Journal of Ambient Computing and Intelligence, vol. 13 (1), pp. 1-19, (IGI Pub)[Ilié 2022]
D. Jaime, J. El Haddad, P. Poizat : “A Preliminary Study of Rhythm and Speed in the Maven Ecosystem” 21^st Belgium-Netherlands Software Evolution Workshop, Mons, Belgium[Jaime 2022]
M. Kerdoudi, T. Ziadi, Ch. Tibermacine, S. Sadou : “Recovering Software Architecture Product Lines” ICECCS 2019 - 24^th International Conference on Engineering of Complex Computer Systems, Nansha, Guangzhou, China, pp. 226-235, (IEEE)[Kerdoudi 2019b]
M. Kerdoudi, T. Ziadi, Ch. Tibermacine, S. Sadou : “A novel approach for Software Architecture Product Line Engineering” Journal of Systems and Software, vol. 186, pp. 111191, (Elsevier)[Kerdoudi 2022]
J. Malenfant : “Towards a well-founded software component model for cyber-physical control systems” Second IEEE International Conference on Robotic Computing, Laguna Hills, California, United States[Malenfant 2018]
J. Martinez, N. Ordoñez, Xh. Tërnava, T. Ziadi, J. Aponte, E. Figueiredo, M. Valente : “Feature Location Benchmark with ArgoUML SPL” Systems and Software Product Line Conference (SPLC), Gothenburg, Sweden[Martinez 2018b]
J. Martinez, T. Ziadi, T. Bissyandé, J. Klein, Y. Le Traon : “Bottom-Up Adoption of Software Product Lines - A Generic and Extensible Approach” 19^th International Software Product Line Conference (SPLC), Nashville, TN, United States, pp. 101-110, (ACM)[Martinez 2015c]
J. Martinez, T. Ziadi, M. Papadakis, T. Bissyandé, J. Klein, Y. Le Traon : “Feature location benchmark for extractive software product line adoption research using realistic and synthetic Eclipse variants” Information and Software Technology, (Elsevier)[Martinez 2018c]
F. Pérez, T. Ziadi, C. Cetina : “Utilizing Automatic Query Reformulations as Genetic Operations to Improve Feature Location in Software Models” IEEE Transactions on Software Engineering, vol. 48 (2), pp. 713-731, (Institute of Electrical and Electronics Engineers)[Pérez 2022]
S. Pinchinat, B. Fila, F. Wacheux, Y. Thierry‑Mieg : “Attack Trees: A Notion of Missing Attacks” GraMSec 2019 - 6^th International Workshop on Graphical Models for Security, vol. 11720, Lecture Notes in Computer Science, Hoboken, NJ, United States, pp. 23-49[Pinchinat 2019]
R. Saddem‑Yagoubi, P. Poizat, S. Houhou : “Business Processes Meet Spatial Concerns: the sBPMN Verification Framework” FM 2021 - 24^th International Symposium on Formal Methods, vol. 13047, Lecture Notes in Computer Science, Beijing, China, pp. 218-234[Saddem-Yagoubi 2021]
A. Sadovykh, A. Bagnato, J. Robin, A. Viehl, T. Ziadi, J. Martinez : “REVAMP: Challenges and innovation roadmap for variability management in round-trip engineering of software-intensive systems” Génie logiciel : le magazine de l'ingénierie du logiciel et des systèmes n°120, pp. 32-36, (Génie industriel multimédia)[Sadovykh 2017]
A. Sangnier, N. Sznajder, M. Potop‑Butucaru, S. Tixeuil : “Parameterized verification of algorithms for oblivious robots on a ring” Formal Methods in System Design, vol. 56, pp. 55-89, (Springer Verlag)[Sangnier 2020]
A. Shatnawi, A.‑D. Seriai, H. Sahraoui, T. Ziadi, A. Seriai : “ReSIde: Reusable Service Identification from Software Families” Journal of Systems and Software, vol. 170, pp. 110748, (Elsevier)[Shatnawi 2020]
A. Shatnawi, T. Ziadi, M. Mohamadi : “Understanding Source Code Variability in Cloned Android Families: an Empirical Study on 75 Families” 2019 26^th Asia-Pacific Software Engineering Conference (APSEC), Putrajava, Malaysia[Shatnawi 2019]
N. Sznajder, B. Bérard, B. Bollig, M. Lehaut : “Parameterized Synthesis for Fragments of First-Order Logic over Data Words” Proceedings of the 23rd International Conference on Foundations of Software Science and Computation Structures (FoSSaCS'20), vol. 12077, Lecture Notes in Computer Science, Dublin, Ireland, pp. 97-118, (Springer)[Sznajder 2020]
V. Vallade, L. Le Frioux, S. Baarir, J. Sopena, V. Ganesh, F. Kordon : “Community and LBD-Based Clause Sharing Policy for Parallel SAT Solving” SAT 2020 - 23rd International Conference on Theory and Applications of Satisfiability Testing, vol. 12178, Lecture Notes in Computer Science, Alghero / Virtual, Italy, pp. 11-27[vallade 2020b]
H. Xu, S. Baarir, T. Ziadi, L. Hillah, S. Essodaigui, Y. Bossu : “Optimisation for the product configuration system of Renault: towards an integration of symmetries” 25^th ACM International Systems and Software Product Line Conference - Volume B, vol. B, SPLC '21: Proceedings of the 25^th ACM International Systems and Software Product Line Conference, Leicester, United Kingdom, pp. 86-90, (ACM)[Xu 2021]

Toutes…