Publications de Jean-Paul BODEVEIX
Zhibin Yang, Zhikai Qiu, Yong Zhou, Zhiqiu Huang, Jean-Paul Bodeveix, M Filali
C2AADL_Reverse: A model-driven reverse engineering approach to development and verification of safety-critical software
Journal of Systems Architecture, 2021, 118, pp.102202. ⟨10.1016/j.sysarc.2021.102202⟩
Zhibin Yang, Shenghao Yuan, Jean-Paul Bodeveix, M Filali, Tiexin Wang, Yong Zhou
Multi-task Ada code generation from synchronous dataflow programs on multi-core: Approach and industrial study
Science of Computer Programming, 2021, Special issue:SI: Formal Techniques for Safety-Critical Systems 2019, 207, pp.102644. ⟨10.1016/j.scico.2021.102644⟩
Zhibin Yang, Yang Bao, Yongqiang Yang, Zhiqiu Huang, Jean-Paul Bodeveix, M Filali, Zonghua Gu
Exploiting augmented intelligence in the modeling of safety-critical autonomous systems
Formal Aspects of Computing, 2021, 33 (3), pp.343-384. ⟨10.1007/s00165-021-00543-6⟩
Jean-Paul Bodeveix, Arnaud Dieumegard, M Filali
Event-B formalization of a variability-aware component model patterns framework
Science of Computer Programming, 2020, 199, ⟨10.1016/j.scico.2020.102511⟩
Fei Wang, Zhibin Yang, Zhi-Qiu Huang, Cheng-Wei Liu, Yong Zhou, Jean-Paul Bodeveix, M Filali
An Approach to Generate the Traceability Between Restricted Natural Language Requirements and AADL Models
IEEE Transactions on Reliability, 2019, 1 (1), pp.1-20. ⟨10.1109/TR.2019.2936072⟩
Zhibin Yang, Jean-Paul Bodeveix, M Filali
Towards a simple and safe Objective Caml compiling framework for the synchronous language SIGNAL
Frontiers of Computer Science, 2019, 13 (4), pp.715-734. ⟨10.1007/s11704-017-6485-y⟩
Elie Fares, Jean-Paul Bodeveix, M Filali
Event algebra for transition systems composition Application to timed automata
Acta Informatica, 2018, 55, pp.363-400. ⟨10.1007/s00236-017-0302-9⟩
Zhibin Yang, Jean-Paul Bodeveix, M Filali, Kai Hu, Yongwang Zhao, Dianfu Ma
Towards a verified compiler prototype for the synchronous language SIGNAL
Frontiers of Computer Science, 2016, 10 (1), pp.37-53. ⟨10.1007/s11704-015-4364-y⟩
Jean-Paul Bodeveix, M Filali, Manuel Garnacho, Régis Spadotti, Zhibin Yang
Towards a verified transformation from AADL to the formal component-based language FIACRE
Science of Computer Programming, 2015, vol. 106, pp. 30-53. ⟨10.1016/j.scico.2015.03.003⟩
Zhibin Yang, Kai Hu, Yong-Wang Zhao, Dian-Fu Ma, Jean-Paul Bodeveix
Verification of AADL Models with Timed Abstract State Machines
Journal of Software, 2015, vol. 26 (n° 2), pp. 202-222
Zhibin Yang, Kai Hu, Dianfu Ma, Jean-Paul Bodeveix, Lei Pi, Jean-Pierre Talpin
From AADL to timed abstract state machine: a certified model transformation
Journal of Systems and Software, 2014, Journal of Systems and Software, pp.20
Zhibin Yang, Kai Hu, Dianfu Ma, Jean-Paul Bodeveix, Lei Pi, Jean-Pierre Talpin
From AADL to Timed Abstract State Machines: A Verified Model Transformation
Journal of Systems and Software, 2014, vol. 93, pp. 42-68. ⟨10.1016/j.jss.2014.02.058⟩
Zhibin Yang, Jean-Paul Bodeveix, Mamoun Filali
A comparative study of two formal semantics of the SIGNAL language
Dans : Frontiers of Computer Science, Springer, Vol. 7 N. 5, p. 673-693, octobre 2013.
Jean-Paul Bodeveix, Mamoun Filali
Event B Development of a Synchronous AADL Scheduler
Dans : Electronic Notes in Theoretical Computer Science (ENTCS), Elsevier, Numéro spécial Proceedings of the B 2011 Workshop, a satellite event of the 17th International Symposium on Formal Methods (FM 2011), Vol. 280, p. 23-33, décembre 2011.
Accès : http://www.sciencedirect.com/science/article/pii/S1571066111001642
BibTeXOdile Nasr, Miloud Rached, Jean-Paul Bodeveix, Mamoun Filali
Spécification et vérification d’un ordonnanceur en B via les automates temporisés
Dans : L’Objet, Hermès Science, Numéro spécial Composants, services et aspects techniques et outils pour la vérification, Vol. 14, N. 4, p. 43-72, décembre 2008.
Miloud Rached, Odile Nasr, Jean-Paul Bodeveix, Mamoun Filali
Une Extension Temporisée de la Méthode B pour la Spécification et la Vérification des Systèmes Temps-Réel
Dans : Journal Européen des Systèmes Automatisés (JESA), Hermès Science, Numéro spécial Approches formelles pour la spécification et la verification des systèmes embarqués temps-réel, Vol. 42 N. 9, p. 1061-1084, décembre 2008.
Jean-Paul Bodeveix, Mamoun Filali, Julia Lawall, Gilles Muller
Automatic Verification of Bossa Scheduler Properties
Dans : Electronic Notes in Theoretical Computer Science (ENTCS), Elsevier, Vol. 185, p. 17-32, juillet 2007.
Jean-Paul Bodeveix, David Chemouil, Mamoun Filali, Martin Strecker
Towards formalising AADL in Proof Assistants
Dans : Electronic Notes in Theoretical Computer Science (ENTCS), Elsevier, Vol. 141, p. 153-169, août 2005.
Richard Banach, Jean-Paul Bodeveix, Mamoun Filali, Michael Poppleton
Dynamic aspects of retrenchments through temporal logic
Dans : Annals of Mathematics, Computing and Teleinformatics (AMCT), Technological Education Institute of Larissa, Grèce, Vol. 1 N. 3, p. 18-26, 2005.
Jean-Paul Bodeveix, Mamoun Filali
Reduction and quantifier elimination techniques for program validation
Dans : Formal Methods in System Design, Vol. 20 N. 1, p. 69-89, 2002.
Jean-Paul Bodeveix, Mamoun Filali, Cesar Munoz
Formalisation de la méthode B en Coq et PVS
Dans : Technique et Science Informatiques, HERMES, PARIS, Vol. 20, N. 7, p. 901-926, juillet 2001.
Didier Plaindoux, Jean-Paul Bodeveix, Christian Percebois
Types versus Classes
Dans : L’Objet, Hermes, Vol. 4, N. 1, p. 3-25, 1998.
Jean-Paul Bodeveix, Mamoun Filali
Techniques de preuve automatique pour la validation de programmes
Dans : Technique et science informatiques, hermes, Paris, Vol. 17, N. 9, p. 1129-1155, novembre 1998.
Jean-Paul Bodeveix, Mamoun Filali
Towards the automatic verification of atomic memory protocols
Dans : Parallel Processing Letter, M. Cosnard, Vol. 7 N. 1, p. 101-112, 1997.
Jean-Paul Bodeveix, Thomas Carle, Elie Fares, Mamoun Filali, Thai Son Hoang
Verifying HyperLTL properties in Event-B
10th International Conference on Rigorous State-Based Methods (ABZ 2024), Jun 2024, Bergame, Italy. pp.255-261, ⟨10.1007/978-3-031-63790-2_20⟩
Quentin Peyras, Jean-Paul Bodeveix, Julien Brunel, David Chemouil
Sound Verification Procedures for Temporal Properties of Infinite-State Systems
33rd International Conference on Computer-Aided Verification (CAV 2021), Jul 2021, Los Angeles (Online), United States
Jian Zhu, Kai Hu, Jean-Paul Bodeveix, M Filali, Jean-Pierre Talpin, Haitao Cao
Formal Simulation and Verification of Solidity contracts in Event-B
45th IEEE Annual Computers, Software, and Applications Conference (COMPSAC 2021), IEEE, Jul 2021, Madrid, Spain. pp.1309-1314, ⟨10.1109/COMPSAC51774.2021.00183⟩
Event-B Formalization of Event-B Contexts
8th International Conference on Rigorous State-Based Methods (ABZ 2021), Jun 2021, Ulm, Germany. pp.66-80, ⟨10.1007/978-3-030-77543-8_5⟩
Jean-Paul Bodeveix, Julien Brunel, David Chemouil, M Filali
Mechanically Verifying the Fundamental Liveness Property of the Chord Protocol
23rd International Symposium on Formal Methods (FM 2019), FME: Formal Methods Europe, Oct 2019, Porto, Portugal. pp.45-63, ⟨10.1007/978-3-030-30942-8_5⟩
Jean-Paul Bodeveix, Arnaud Dieumegard, M Filali
Event-B Formalization of a Variability-Aware Component Model Patterns Framework
15th International Conference on Formal Aspects of Component Software (FACS 2018), Oct 2018, Pohang, South Korea. pp.54-74, ⟨10.1007/978-3-030-02146-7_3⟩
Jean-Paul Bodeveix, Arnaud Dieumegard, M Filali
Pattern-based requirements development
9th European Congress on Embedded Real Time Software and Systems (ERTS 2018), Jan 2018, Toulouse, France
Jean-Paul Bodeveix, M Filali, Shuanglong Kan
A Refinement-based compiler development for synchronous languages
15th ACM-IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE 2017), Sep 2017, Vienna, Austria. pp.165-174, ⟨10.1145/3127041.3127056⟩
Jean-Paul Bodeveix, M Filali, Shuanglong Kan
A refinement-based compiler development for synchronous languages
15th International Conference on Formal Methods and Models for System Design (MEMOCODE 2017), ACM; SIGBED; SIGDA; IEEE CEDA; IEEE CAS, Sep 2017, Vienne, Austria. pp.165-174, ⟨10.1145/3127041.3127056⟩
Badr Siala, Jean-Paul Bodeveix, M Filali, Tahar Bhiri
Automatic Refinement for Event-B through Annotated Patterns
25th Euromicro International Conference on Parallel, Distributed and network-based Processing (PDP 2017), Mar 2017, Saint Petersburg, Russia. pp.287-290, ⟨10.1109/PDP.2017.72⟩
Badr Siala, Tahar Bhiri, Jean-Paul Bodeveix, M Filali
An Event-B Development Process for the Distributed BIP Framework
18th International Conference on Formal Engineering Methods (ICFEM 2016), Nov 2016, Tokyo, Japan. pp. 313-328
Badr Siala, Mohamed Tahar Bhiri, Jean-Paul Bodeveix, M Filali
Un processus de développement Event-B pour des applications distribuées
15emes Journéees Approches Formelles dans l’Assistance au Développement de Logiciels (AFADL 2016), en collaboration avec les journées du GDR GPL, Jun 2016, Besançon, France. pp.94-100
Badr Siala, Tahar Bhiri, Jean-Paul Bodeveix, M Filali
An Event-B development process for the distributed BIP framework (Journées FAC Toulouse 2016)
Journées Formalisation des Activités Concurrentes (FAC 2016), Groupe IFSE du RTRA STAE (Réseau Thématique de Recherche Avancée « Sciences et Technologies pour l’Aéronautique et l’Espace » de Toulouse), Mar 2016, Toulouse, France
Zhibin Yang, Jean-Paul Bodeveix, M Filali
Multi-core Code Generation from Polychronous Programs with Time-Predictable Properties (ACVI 2014)
1st International Workshop on Architecture Centric Virtual Integration (ACVI 2014), Sep 2014, Valencia, Spain. pp.1-10
Zhibin Yang, Jean-Paul Bodeveix, M Filali, Kai Hu, Dianfu Ma
A Verified Transformation: From Polychronous Programs to a Variant of Clocked Guarded Actions
17th International Workshop on Software and Compilers for Embedded Systems (SCOPES 2014), SIGBED: Special Interest Group on Embedded Systems, Jun 2014, Sankt Goar, Germany. pp.128-137, ⟨10.1145/2609248.2609259⟩
Elie Fares, Jean-Paul Bodeveix, Mamoun Filali
Event Algebra for Transition Systems Composition – Application to Timed Automata (regular paper)
Dans : International Symposium on Temporal Representation and Reasoning (TIME 2013), Penscacolq, FL, USA, 26/09/13-28/09/13, IEEE Computer Society – Conference Publishing Services, p. 125-132, 2013.
Elie Fares, Jean-Paul Bodeveix, Mamoun Filali, Manuel Garnacho
An Automatic Technique for Checking the Simulation of Timed Systems (regular paper)
Dans : Automated Technology for Verification and Analysis, Hanoi, Vietnam, 15/10/13-18/10/13, Vol. 8172, Springer-Verlag, Lecture Notes in Computer Science, p. 71-86, octobre 2013.
Abdeldjalil Boudjadar, Frits Vaandrager, Jean-Paul Bodeveix, Mamoun Filali
Extending UPPAAL for the Modeling and Verification of Dynamic Real-Time Systems (regular paper)
Dans : Fundamentals of Software Engineering (FSEN 2013), Tehran, Iran, 24/04/13-26/04/13, Vol. 8161, Springer, Lecture Notes in Computer Science, p. 111-132, avril 2013.
Manuel Garnacho, Jean-Paul Bodeveix, Mamoun Filali
A Mechanized Semantic Framework for Real-Time Systems (regular paper)
Dans : International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS 2013), Buenos Aires, Argentina, 29/08/13-31/08/13, Victor Braberman, Laurent Fribourg (Eds.), Springer, p. 106-120, août 2013.
Abdeldjalil Boudjadar, Jean-Paul Bodeveix, Mamoun Filali
Compositional Refinement for Real-Time Systems with Priorities (regular paper)
Dans : International Symposium on Temporal Representation and Reasoning (TIME 2012), Leicester, United Kingdom, 12/09/12-14/09/12, IEEE Computer Society, p. 57-64, septembre 2012.
Bernard Berthomieu, Jean-Paul Bodeveix, Silvano Dal Zilio, Patrick Farail, Mamoun Filali, Pierre Gaufillet, François Vernadat
La traduction AADL-FIACRE: l’expérience TOPCASED (regular paper)
Dans : Approches Formelles dans l’Assistance au Développement de Logiciels (AFADL 2012), Grenoble, 11/01/12-13/01/12 (conférencier invité), LCIS/LIG Grenoble, p. 8-8, janvier 2012.
Elie Fares, Jean-Paul Bodeveix, Mamoun Filali
Design of a BPEL verification tool (regular paper)
Dans : International Workshop on Web Services and Formal Methods, Clermont-Ferrand, 01/09/11-02/09/11, Springer, p. 95-109, février 2012.
Jean-Paul Bodeveix, Mamoun Filali
Event B development of a synchronous AADL scheduler (regular paper)
Dans : Workshop B 2011, colocated with FM 2011, Limerick, Ireland, 21/06/11-21/06/11, University of Limerick, (support électronique), juin 2011.
Jean-Paul Bodeveix, Abdeldjalil Boudjadar, Mamoun Filali
An Alternative Definition for Timed Automata Composition (regular paper)
Dans : Automated Technology for Verification and Analysis, Taipei, Taiwan, 11/10/11-14/10/11, Vol. 6996, Springer-Verlag, Lecture Notes in Computer Science, p. 105-119, octobre 2011.
Elie Fares, Jean-Paul Bodeveix, Mamoun Filali
A Transformation and Verification Framework for BPEL
Dans : Services et Langages et modèles à l’exécution, LILLE GDR GPL, 10/06/11-10/06/11.
Marie de Roquemaurel, Jean-Paul Bodeveix, Mamoun Filali
Réécriture de contraintes OCL (regular paper)
Dans : Journées sur l’Ingénierie Dirigée par les Modèles (IDM 2011), Lille, 07/06/11-10/06/11, CNRS – GDR GPL, p. 127-133, 2011.
Marie de Roquemaurel, Thomas Polacsek, Jean-François Rolland, Jean-Paul Bodeveix, Mamoun Filali
Assistance à la conception de modèles à l’aide de contraintes (regular paper)
Dans : Journées nationales du Groupement De Recherche CNRS du Génie de la Programmation et du Logiciel (GDR-GPL), Groupe de travail MFDL, Lille, 07/06/11-10/06/11, CNRS – GDR GPL, p. 121-136, juin 2011.
Elie Fares, Jean-Paul Bodeveix, Mamoun Filali
Verification of Timed BPEL 2.0 Models (regular paper)
Dans : Business Process Modeling, Development and Support (BPMDS 2011), London, 20/06/11-21/06/11, Terry Halpin, Selmin Nurcan, John Krogstie, Pnina Soffer, Erik Proper (Eds.), Springer, LNBIP 81, p. 261-275, juin 2011.
Zhibin Yang, Hu Kai, Jean-Paul Bodeveix, Lei Pi, Dianfu Ma, Jean-Pierre Talpin
Two formal semantics of a subset of AADL (regular paper)
Dans : UML&AADL, Las Vegas, 27/04/11-27/04/11, IEEE Computer Society, ICECCS ’11, p. 344-349, avril 2011.
Marie de Roquemaurel, Jean-Paul Bodeveix, Mamoun Filali, Frédéric Minot
Model design through constraint solving
Dans : TOPCASED DAYS, Toulouse, 02/02/11-04/02/11.
Tiago Correa, Leandro Becker, Jean-Paul Bodeveix, J.-M. Farines, Mamoun Filali, François Vernadat
Supporting the Design of Safety Critical Systems Using AADL (regular paper)
Dans : , Oxford, 22/03/10-26/03/10, IEEE Computer Society, p. 331-336, mars 2010.
Zhibin Yang, Kai Hu, Lei Pi, Jean-Paul Bodeveix, Dianfu Ma
Formal Semantics and Verification of AADL Modes in Timed Abstract State Machine (regular paper)
Dans : International Conference on Progress in Informatics and Computing, Shanghai, China, 10/12/10-12/12/10, Vol. 2, IEEExplore digital library, p. 1098-1103, décembre 2010.
Marie de Roquemaurel, Thomas Polacsek, Jean-François Rolland, Jean-Paul Bodeveix, Mamoun Filali
Assistance à la conception de modèles à l’aide de contraintes (regular paper)
Dans : Approches Formelles dans l’Assistance au Développement de Logiciels (AFADL 2010), Poitiers, 09/06/10-11/06/10, Yamine Ait-Ameur (Eds.), LISI-ENSMA, p. 181-196, juin 2010.
Loïc Besnard, Thierry Gautier, Julien Ouy, Jean-Pierre Talpin, Jean-Paul Bodeveix, Alexandre Cortier, Marc Pantel, Martin Strecker, Gérald Garcia, Ana-Helena Rugina, Jérémy Buisson, Fabien Dagnat
Polychronous Interpretation of Synoptic, a Domain Specific Modeling Language for Embedded Flight-Software (regular paper)
Dans : Workshop on Formal Methods for Aerospace (FMA 2009), Eindhoven, 03/11/09, Vol. 20, Manuela Bujorianu, Michael Fisher (Eds.), Electronic Proceedings in Theoretical Computer Science (EPTCS), p. 80-87, mars 2010.
Bernard Berthomieu, Jean-Paul Bodeveix, Silvano Dal Zilio, Pierre Dissaux, Mamoun Filali, Pierre Gaufillet, Sebastien Heim, François Vernadat
Formal Verification of AADL models with Fiacre and Tina (regular paper)
Dans : European Congress on Embedded Real-Time Software (ERTS 2010), Toulouse, 19/05/10-21/05/10, SIA/3AF/SEE, (support électronique), 2010.
Accès : http://web1.see.asso.fr/erts2010/Site/0ANDGY78/Fichier/PAPIERS%20ERTS%202010%202/ERTS2010_0107_final.pdf
BibTeXTiago Correa, Leandro Becker, Jean-Paul Bodeveix, J.-M. Farines, Mamoun Filali, François Vernadat
Verification Based Development Process for Embedded Systems (regular paper)
Dans : European Congress on Embedded Real-Time Software (ERTS 2010), Toulouse, 19/05/10-21/05/10, Société des Ingénieurs de l’Automobile, (support électronique), mai 2010.
Accès : http://web1.see.asso.fr/erts2010/Site/0ANDGY78/Fichier/PAPIERS%20ERTS%202010/ERTS2010_0029_final.pdf
BibTeXAlexandre Cortier, Jean-Paul Bodeveix, Marc Pantel, Martin Strecker, Gérald Garcia, Eric Morand, Ana-Helena Rugina, Jean-Pierre Talpin
Synoptic : a Domain Specific Modeling Language for Embed- ded Real-Time Flight Software Design (regular paper)
Dans : European Conference on Embedded Real Time Software and Systems (ERTS 2010), Toulouse, 19/05/10-21/05/10, SIA/3AF/SEE, (support électronique), mai 2010.
Lei Pi, Jean-Paul Bodeveix, Mamoun Filali, Hu Kai, Ma Dianfu
A comparative study of FIACRE and TASM to define AADL real time concepts
Dans : UML&AADL’2009 – 14th IEEE International Conference on Engineering of Complex Computer Systems, Postdam, 02/06/09-04/06/09, IEEE : Institute of Electrical and Electronics Engineers, p. 347-352, juin 2009.
Accès : http://www2.computer.org/portal/web/csdl/abs/proceedings/iceccs/2009/3702/00/piceccs200900toc.htm
BibTeXRicardo Bedin Franca, Leandro Buss Becker, Jean-Paul Bodeveix, J.-M. Farines, Mamoun Filali
Towards Safe Design of Synchronous Bus Protocols in Event-B (regular paper)
Dans : Brazilian Symposium on Formal Methods, Gramado Brésil, 19/08/09-21/08/09, Brazilian Computer Society, p. 171-186, août 2009.
Bernard Berthomieu, Jean-Paul Bodeveix, Christelle Chaudet, Silvano Dal Zilio, Mamoun Filali, François Vernadat
Formal Verification of AADL Specifications in the Topcased Environment
Dans : International Conference on Reliable Software Technologies – Ada-Europe, Brest, France, 08/06/09-12/06/09, Springer-Verlag, lncs 5570, p. 207-221, 2009.
Lei Pi, Jean-Paul Bodeveix, Mamoun Filali
Modeling AADL Data Communication with BIP
Dans : International Conference on Reliable Software Technologies – Ada-Europe, Telecom Bretagne, Brest, France, 08/06/09-12/06/09, Springer-Verlag, lncs 5570, p. 192-206, 2009.
Lei Pi, Zhibin Yang, Jean-Paul Bodeveix, Mamoun Filali, Kai Hu
A comparative study of two Real-Time formalisms: FIACRE and TASM (regular paper)
Dans : IEEE Real-Time Systems Symposium (Work-In-Progress track) (RTSS 2008), Barcelone, 30/11/08-03/12/08, IEEE : Institute of Electrical and Electronics Engineers, (support électronique), décembre 2008.
Jean-François Rolland, Jean-Paul Bodeveix, Mamoun Filali, David Chemouil, Thomas Dave
AADL modes for space software
Dans : Data Systems In Aerospace (DASIA 2008), Palma de Majorca-Spain, 27/05/08-30/05/08, European Space Agency (ESA Publications), (support électronique), mai 2008.
Jean-François Rolland, Jean-Paul Bodeveix, Mamoun Filali, David Chemouil, Thomas Dave
Modes in asynchronous systems
Dans : IEEE International Conference on Engineering Complex Computer Systems (ICECCS 2008), Belfast Ireland, 31/03/08-04/04/08, IEEE : Institute of Electrical and Electronics Engineers, (support électronique), avril 2008.
Frédéric Minot, Jean-Paul Bodeveix, Mamoun Filali, David Doose, Charles Castel, Cédric Pralet, P. Bieber
Constraint-based design of Avionics platform- preliminary design exploration
Dans : European Congress on Embedded Real-Time Software (ERTS 2008), Toulouse, 31/01/08-01/02/08, Société de l’Electricité, de l’Electronique et des Technologies de l’Information et de la Communication (SEE), (support électronique), janvier 2008.
Patrick Farail, Pierre Gaufillet, Florent Peres, Jean-Paul Bodeveix, Mamoun Filali, Bernard Berthomieu, Saad Rodrigo, François Vernadat, Hubert Garavel, Frédéric Lang
FIACRE: an intermediate language for model verification in the TOPCASED environment
Dans : European Congress on Embedded Real-Time Software (ERTS 2008), Toulouse, 29/01/08-01/02/08, Société de l’Electricité, de l’Electronique et des Technologies de l’Information et de la Communication (SEE), (support électronique), janvier 2008.
Jean-François Rolland, Jean-Paul Bodeveix, David Chemouil, Mamoun Filali, Dave Thomas
Towards a formal semantics for AADL execution model
Dans : European Congress on Embedded Real-Time Software (ERTS 2008), Toulouse, 29/01/08-01/02/08, SIA/3AF/SEE, (support électronique), janvier 2008.
Ricardo Bedin Franca, Daniel Gobbi, J.-M. Farines, Jean-Paul Bodeveix, Leandro Becker
Design of Real-Time Automation Systems Using Architecture Description Languages
Dans : Simpósio Brasileiro de Automação Inteligente (SBAI 2007), Florianópolis – Brasil, 08/08/07-11/08/07, Sociedade Brasileira de Automática (SBA), (support électronique), août 2007.
Ricardo Bedin Franca, Jean-François Rolland, Jean-Paul Bodeveix, Mamoun Filali
Assessment of AADL’s behavioral annex
Dans : FAC Formalisation des Activités Concurrentes, Toulouse, 15/03/07-16/03/07.
Ricardo Bedin Franca, Jean-Paul Bodeveix, Mamoun Filali
AADL Modeling of a Generic Bus
Dans : FAC, Toulouse, 15/03/07-16/03/07.
Julien Brunel, Frédéric Cuppens, Nora Cuppensboulahia, Thierry Sans, Jean-Paul Bodeveix
Security Policy Compliance with Violation Management
Dans : ACM Workshop on Formal Methods in Security Engineering: From Specifications to Code, Washingthon USA, 12/11/07-13/11/07, ACM : Association for Computing Machinery, p. 31-40, novembre 2007.
Jean-Paul Bodeveix, Raphael Cavallero, David Chemouil, Mamoun Filali, Jean-François Rolland
A mapping from AADL to Java-RTSJ
Dans : International Workshop on Java Technologies for Real-time and Embedded Systems (JTRES 2007), Vienna, Austria, 26/09/07-28/09/07, ACM : Association for Computing Machinery, ACM International Conference Proceeding Series, p. 165-174, septembre 2007.
Ricardo Bedin Franca, Jean-Paul Bodeveix, Mamoun Filali, David Chemouil, Dave Thomas
The AADL behaviour annex — experiments and roadmap
Dans : IEEE International Conference on Engineering Complex Computer Systems (ICECCS 2007), Auckland, New Zealand, 11/07/07-14/07/07, IEEE Computer Society, p. 377-382, 2007.
Ricardo Bedin Franca, J.-M. Farines, Jean-Paul Bodeveix, Leandro Becker, Mamoun Filali
Modelling a bus protocol an incremental approach
Dans : Workshop on Real-Time Systems (WTR 2007), Belem (Brésil)l, 28/05/07-28/05/07, Universidade Federal de Santa Catarina, (support électronique), mai 2007.
Jean-Paul Bodeveix, David Chemouil, Mamoun Filali, Nicolas Lalevee, Martin Strecker
Towards the verification of model transformations
Dans : European Congress on Embedded Real-Time Software (ERTS 2006), Toulouse, 25/01/06-27/01/06, Société des Ingénieurs de l’Automobile, (support électronique), 2006.
Accès : http://www.sia.fr/evenement_detail_erts2006_embedded_real_time_actes_365.htm
BibTeXJean-Paul Bodeveix, Pierre Dissaux, Patrick Farail, Mamoun Filali, Pierre Gaufillet, François Vernadat
Behavioural descriptions in architecture description languages: Application to AADL
Dans : European Congress on Embedded Real-Time Software (ERTS 2006), Toulouse, 25/01/06-27/01/06, Société des Ingénieurs de l’Automobile, (support électronique), 2006.
Accès : http://www.sia.fr/evenement_detail_erts2006_embedded_real_time_actes_365.htm
BibTeXJean-Paul Bodeveix, Mamoun Filali, Julia Lawall, Gilles Muller
Automatic Verification of Bossa Scheduler Properties
Dans : nternational Workshop on Automated Verification of Critical Systems (AVOCS 2006), LORIA Nancy, 18/09/06-19/09/06, Archives ouvertes HAL, (en ligne), septembre 2006.
Accès : http://hal.inria.fr/
BibTeXJulien Brunel, Jean-Paul Bodeveix, Mamoun Filali
A state/event temporal deontic logic
Dans : Journées FAC’06, Toulouse, 23/03/06-24/03/06.
Jean-Paul Bodeveix, Pierre Dissaux, Mamoun Filali, Pierre Gaufillet, François Vernadat
AADL behavioural annex
Dans : Data Systems In Aerospace (DASIA 2006), Berlin-Germany, 22/05/06-25/05/06, European Space Agency (ESA Publications), (support électronique), 2006.
Jean-Paul Bodeveix, Mamoun Filali, Miloud Rached, David Chemouil, Pierre Gaufillet
Experimenting an AADL Behavioural Annex and a Verification Method
Dans : Data Systems In Aerospace (DASIA 2006), Berlin-Germany, 22/05/06-25/05/06, European Space Agency (ESA Publications), (support électronique), 2006.
Julien Brunel, Jean-Paul Bodeveix, Mamoun Filali
A state/event temporal deontic logic
Dans : International Workshop on Deontic Logic in Computer Science (DEON 2006), Utrecht, The Netherlands, 12/07/06-14/07/06, Vol. , Lou Goble, John-Jules Ch. Meyer (Eds.), Springer, LNAI 4048, p. 85-100, juillet 2006.
Jean-Paul Bodeveix, Mamoun Filali, Julia Lawall, Gilles Muller
Vérification automatique de propriétés d’ordonnanceurs Bossa
Dans : Approches Formelles dans l’Assistance au Développement de Logiciels (AFADL 2006), ENST Paris, 15/03/06-17/03/06, ENST, p. 95-109, mars 2006.
Odile Nasr, Jean-Paul Bodeveix, Mamoun Filali, Miloud Rached
Développement validé d’odonnanceurs en B
Dans : Approches Formelles dans l’Assistance au Développement de Logiciels (AFADL 2006), ENST Paris, 15/03/06-17/03/06, ENST, p. 79-93, mars 2006.
Odile Nasr, Jean-Paul Bodeveix, Mamoun Filali, Miloud Rached
Verification of a Scheduler in B Through a Timed Automata Specification
Dans : Annual ACM Symposium on Applied Computing (SAC 2006), Dijon, 23/04/06-27/04/06, ACM : Association for Computing Machinery, p. 1800-1801, avril 2006.
Miloud Rached, Jean-Paul Bodeveix, Mamoun Filali, Odile Nasr
Real Time Aspects: Specification and Composition in B
Dans : 7th International Workshop on Aspect-Oriented Modeling, Montego Bay, Jamaica, 02/10/05-02/10/05, ?, octobre 2005.
Accès : http://dawis.informatik.uni-essen.de/events/AOM_MODELS2005/papers.shtml
BibTeXJean-Paul Bodeveix, Mamoun Filali, Julia Lawall, Gilles Muller
Applying the B formal method to the Bossa domain-specific language
Dans : The 17th Nordic Workshop on Programming Theory, Copenhagen, Denmark, 19/10/05-21/10/05, DIKU Copenhagen, Denmark, octobre 2005.
Miloud Rached, Jean-Paul Bodeveix, Mamoun Filali, Odile Nasr
A Timed B Method for Modelling Real Time Reactive Systems
Dans : SEEFM05. 2nd South-East European Workshop on Formal Methods, Ohrid (Macédoine), 18/11/05-20/11/05, South-East European Research Center (SEERC), p. 181-195, novembre 2005.
Jean-Paul Bodeveix, Ousmane Koné, Rachid Bouaziz
Test method for embedded real-time systems
Dans : ERCIM European Workshop on Dependable Software Intensive Embedded Systems, Porto, 31/08/05-02/09/05, ERCIM, p. 1-10, août 2005.
Richard Banach, Jean-Paul Bodeveix, Mamoun Filali, Michael Poppleton
Dynamic aspects of retrenchments through temporal logic
Dans : SEEFM05 2nd South-East European Workshop on Formal Methods, Ohrid (Macédoine), 18/11/05-19/11/05, South-East European Research Center (SEERC), p. 104-118, novembre 2005.
Jean-Paul Bodeveix, Mamoun Filali, Julia Lawall, Gilles Muller
Formal methods meet domain specific languages
Dans : Fifth International Conference on Integrated Formal Methods (IFM), Eindhoven Netherlands, 29/11/05-02/12/05, LNCS (springer verlag) Vol. 3771, p. 187-206, novembre 2005.
Jean-Paul Bodeveix, David Chemouil, Mamoun Filali, Martin Strecker
Towards formalizing AADL in proof assistants
Dans : Formal Foundations of Embedded software and component-based softare architectures (ETAPS), Edinburgh, 02/04/05-10/04/05, Juliana Kuster-Filipe, Iman Poernomo , Ralf Reussner, Sandeep Shukla (Eds.), LFCS (University of Edinburgh), p. 137-153, avril 2005.
Jean-Paul Bodeveix, Mamoun Filali, Martin Strecker
Towards formalising AADL in Proof Assistants
Dans : Journées FAC’05, Toulouse LAAS, 09/03/05-10/04/05.
Odile Nasr, Miloud Rached, Jean-Paul Bodeveix, Mamoun Filali
Specification of real-time schedulers
Dans : 16th Euromicro Conference on Real-Time Systems (ECRTS’04) (Work In Progress Session), Catania, Italy, 30/06/04-02/07/04, -, juin 2004.
Nouhad Amaneddine, Jean-Paul Bahsoun, Jean-Paul Bodeveix
Vers une transformation avancée de données structurées
Dans : MAJESTIC, Calais, France, 13/10/04-15/10/04, Maison de la Recherche Blaise Pascal, octobre 2004.
Nouhad Amaneddine, Jean-Paul Bahsoun, Jean-Paul Bodeveix
TransM: A Structured Document Transformation Model
Dans : 3rd International Conference on Information Systems Technology and its Applications (ISTA), Salt Lake City, Utah, USA, 15/07/04-17/07/04, Lecture Notes in Informatics, p. 53-66, juillet 2004.
Jean-Paul Bodeveix, Mamoun Filali, Odile Nasr
Spécification d’ordonnanceurs temps réel
Dans : FAC, Toulouse, 09/03/04-10/03/04.
Jean-Paul Bodeveix, Mamoun Filali, Miloud Rached
Méthodes de spécification de systèmes temps réel en B
Dans : FAC, Toulouse, 09/03/04-10/03/04.
Jean-Paul Bodeveix, Mamoun Filali
About disjunctive invariants in UPPAAL
Dans : NWPT, Turku Finlande, 29/10/03-31/10/03.
Pierre Bazex, Jean-Paul Bodeveix, Christophe Le Camus, Thierry Millan, Christian Percebois
Vérification de modèles UML fondée sur OCL
Dans : INFORSID, Nancy, 03/06/03-06/06/03, Congrès INFormatique des ORganisations et Systèmes d’Information et de Décision (INFORSID), p. 185-200, juin 2003.
Bernard Berthomieu, P.-O. Ribet, François Vernadat, J.-L. Bernartt, J.-M. Farines, Jean-Paul Bodeveix, Mamoun Filali, Gérard Padiou, Pierre Michel, Patrick Farail, Pierre Gaufillet, Pierre Dissaux, Jean-Luc Lambert
Towards the verification of real-time systems in avionics: TheCotre approach
Dans : Eigth International workshop for industrial critical systems, ROROS, 05/06/03-07/06/03, Thomas Arts, Wan Fokkink, p. 201-216, juin 2003.
Accès : http://www.elsevier.nl/locate/entcs/volume80.html
BibTeXJ.-M. Farines, Bernard Berthomieu, Jean-Paul Bodeveix, Pierre Dissaux, Patrick Farail, Mamoun Filali, Pierre Gaufillet, Hicham Hafidi, Jean-Luc Lambert, Pierre Michel, François Vernadat
The Cotre project: rigorous development for real time systems in Avionics
Dans : WRTP’03 27th IFAC/IFIP/IEEE Workshop on real-time programming, Logow(Pologne), 14/05/03-17/05/03, IEEE, p. 51-56, mai 2003.
Jean-Paul Bodeveix, Mamoun Filali
Machines virtuelles pour le B événementiel
Dans : AFADL, Rennes, 15/01/03-17/01/03, Jean-Marc Jézéquel, INRIA, p. 227-241, janvier 2003.
Accès : http://www.irisa.fr/manifestations/2003/AFADL03
BibTeXJean-Paul Bodeveix, Mamoun Filali
Machines virtuelles pour le B événementiel
Dans : Journées GDR B, Paris, 13/06/02-14/06/02.
Accès : http://www-lsr.imag.fr/B/Documents/CNAM-2002-06-13/prog-CNAM-2002.html
BibTeXJean-Paul Bodeveix, Mamoun Filali, Semra Sarpdag
Etude des files de priorité
Dans : journée GDR B, Nantes, 29/11/02-29/11/02.
Accès : http://www-lsr.imag.fr/B/Documents/Nantes-2002-11-29/prog.html
BibTeXJean-Paul Bodeveix, Mamoun Filali
Un outil pour la description de types inductifs en B
Dans : journée du GDR B, Nantes, 29/11/02-29/11/02.
Accès : http://www-lsr.imag.fr/B/Documents/Nantes-2002-11-29/prog.html
BibTeXJean-Paul Bodeveix, Thierry Millan, Christian Percebois, Christophe Le Camus, Pierre Bazex, Louis Féraud, Ralph Sobek
Extending OCL for verifying UML models consistency
Dans : Workshop on Consistency Problems in UM- based Software Development in conjonction with the fifth International Conference on the Unified Modelling Language “UML” 2002 “Modelling Languages, Concepts and Tools”, Dresden, Allemagne, 01/10/02, Ludwik Kuzniarz – Gianna Reggio – Jean-Louis Sourrouille – Zbigniew Huzar, p. 75-91, octobre 2002.
Jean-Paul Bodeveix, Mamoun Filali
Type Synthesis in B and the Translation of B to PVS
Dans : ZB’2002, Grenoble, 23/01/02-25/01/02, springer verlag, p. 350-369, janvier 2002.
Jean-Paul Bodeveix, Mamoun Filali, Cesar Munoz
Formalisation de la méthode B en Coq et PVS
Dans : AFADL, Grenoble, 26/01/00-28/01/00, LSR/IMAG, p. 96-110, janvier 2000.
Accès : http://www-lsr.imag.fr/afadl
BibTeXPierre Bazex, Jean-Paul Bodeveix, Louis Féraud, Thierry Millan
Modélisation et transformations de données
Dans : Journées sur les technologies applicables à la valorisation de données, Toulouse, .
Pierre Bazex, Jean-Paul Bodeveix, Louis Féraud, Thierry Millan, Christian Percebois
Data Design and Transformation
Dans : World Multiconference on Systemics, Cybernetics and Informatics 2000, Orlando (USA), 23/07/00-26/07/00, IIIS, 14269 Lord Barclay Dr., Orlandom FL 32837, USA, p. 587-592, juillet 2000.
Jean-Paul Bodeveix, Mamoun Filali, Daniel Le Berre
Expression de méthodes de validation. Transformation en logique propositionnelle ou monadique
Dans : Journées de VERIFICATION FORMELLE, ORLEANS, 08/06/00-09/06/00.
Accès : http://www.univ-orleans.fr/SCIENCES/LIFO/Manifestations/Jo-VERIF/
BibTeXJean-Paul Bodeveix, Mamoun Filali
Expérimentation de méthodes d’accélération pour la validation de systèmes paramétrés
Dans : FAC’2000, Toulouse, 18/05/00, IRIT, p. 19-29, mai 2000.
Jean-Paul Bodeveix, Mamoun Filali
FMona: a tool for expressing validation techniques over infinite state systems
Dans : Tools and algorithms for the construction and analysis of systems (TACAS), Berlin, 27/03/00-31/03/00, Springer, p. 204-219, mars 2000.
Salam Majoul, Christian Percebois, Jean-Paul Bodeveix
A Concurrent Object-Based Model and its Use for Coordinating Java Components
Dans : TOOLS – Technology of Object-Oriented Languages and Systems, Santa Barbara, 01/08/99-05/08/99, IEEE, p. 15-25, août 1999.
Jean-Paul Bodeveix, Mamoun Filali
Un outil générique pour l’expression de méthodes de validation
Dans : Journées Modélisation et Vérification, Besançon, 09/12/99-11/12/99.
Jean-Paul Bodeveix, Mamoun Filali, Cesar Munoz
Mécanisation de la méthode B en Coq et PVS
Dans : Journées BUG-SEE, LILLE, 29/11/99-30/11/99.
Jean-Paul Bodeveix, Mamoun Filali, Cesar Munoz
A Formalization of the B method in Coq and PVS
Dans : FM’99 — B Users Group Meeting — Applying B in an industrial context : Tools, Lessons and Techniques, Toulouse, Springer-Verlag, p. 32-48, septembre 1999.
Jean-Paul Bodeveix, Mamoun Filali
A generic tool for expressing the development of validations
Dans : 11th Nordic Workshop on Programming Theory NWPT’99, Uppsala, 06/10/99-08/10/99, Bjorn Victor and Wang Yi, Uppsala University, p. 37-37, octobre 1999.
Jean-Paul Bodeveix, Mamoun Filali
Preuve automatique par abstraction de problèmes à espace d’états infini ou paramétrés
Dans : Formalisation des activités concurrentes, LAAS Toulouse, 25/02/99-26/02/99, LAAS, p. 19-30, février 1999.
Jean-Paul Bodeveix, Mamoun Filali
On the automatic validation of parameterized Unity programs
Dans : Workshop on formal methods for parallel programming: theory and applications, Orlando , 03/04/98-03/04/98, lncs vol. 1388, Berlin, Germany, p. 820-832, avril 1998.
Jean-Paul Bodeveix, Mamoun Filali
Expériences de preuves assistées et automatiques de problèmes paramétrés
Dans : Journées Modélisation et Vérification, CIRM, Marseille, 16/12/98-18/12/98.
Salam Majoul, Christian Percebois, Jean-Paul Bodeveix
Reasoning about Negative Conditions in a Concurrent Rewriting System
Dans : 2nd France-Japan Workshop on Object-Based Parallel and Distributed Computation, Toulouse, .
Jean-Paul Bodeveix, Mamoun Filali
Preuve automatique de propriétés de sureté
Dans : GDR de Programmation – Journées du pôle Preuves et Spécifications Algébriques, –, .
Jean-Paul Bodeveix, Mamoun Filali
Validation de développements
Dans : AFADL Approches formelles dans l’assistance au développement de logiciels, CERT Toulouse, GDR de Programmation: Pôle preuves et spécifications algébriques, p. 165-176, mai 1997.
Jean-Paul Bodeveix, Dominique Carrière, Mamoun Filali
A refinement-based validation of a cache coherence protocol
Dans : 10th International Conference on Parallel and Distributed Computing Systems, New Orleans, Louisiana USA, ISCA, p. 332-337, octobre 1997.
Jean-Paul Bodeveix, Christian Percebois, Salam Majoul
An object oriented coordination model based on multiset rewriting
Dans : Procs. of ninth International Conference on Parallel and Distributed Computing Systems, Dijon, 25/09/96-27/09/96, isca, p. 1-12, septembre 1996.
Jean-Paul Bodeveix, Mamoun Filali
Formalisation et validation de protocoles de cohérence mémoire atomique
Dans : École ISYPAR, IRIT, .
Jean-Paul Bodeveix, Mamoun Filali
Spécification et raffinement de modèles de cohérence mémoire
Dans : FAC96: Formalisation des Applications Concurrentes, Toulouse, 07/02/96-08/02/96, -, février 1996.
Jean-Paul Bodeveix, Dominique Carrière, Mamoun Filali
Etude du protocole de cohérence de la machine M3S
Dans : Rencontres du parallélisme RenPar’8, –, -, p. 173-176, mai 1996.
Jean-Paul Bodeveix, Mamoun Filali
Spécification et raffinement de modèles de cohérence mémoire
Dans : Modélisation des systèmes réactifs, –, AFCET, mars 1996.
Jean-Paul Bodeveix, Mamoun Filali
Towards the automatic verification of memory protocols
Dans : International Workshop on Formal methods for parallel programming, _, IEEE, avril 1996.
Jean-Paul Bodeveix, Christian Percebois, Salam Majoul
Multiset Rewriting for Concurrent Object-Oriented Programming
Dans : ECOOP’96 Workshop on Proof Theory of Concurrent Object-Oriented Programming, Linz, Austria, -, juillet 1996.
Jean-Paul Bodeveix, Mamoun Filali
On the Refinement of Symmetric Memory Protocols
Dans : Higher Order Logic Theorem Proving and its Applications, –, Springer-Verlag, LNCS 971, p. 58-74, septembre 1995.
Jean-Paul Bodeveix, Mamoun Filali, Pierre Roché
Sémantique des modèles de consistance mémoire
Dans : Journée du pôle preuves et spécifications algébriques du GDR programmation, –, .
Jean-Paul Bodeveix, Mamoun Filali, Pierre Roché
Towards a HOL theory of memory
Dans : Higher Order Logic Theorem Proving and its Applications, –, Springer-Verlag, LNCS 859, p. 49-64, septembre 1994.
Juan-Carlos Cruellas, Jean-Paul Bodeveix, Thierry Millan, Agusti Canals
The NEPTUNE Technology to verify and to Document Software cOMPONENTS
Dans : Business Component-Based Software Engineering. Franck Barbier (Eds.) , Kluwer Academic Publishers, Post Office Box 322 – 330 AH Dordrecht – THE NETHERLANDS, p. 101-118, 2003.
Méthodes formelles et sûreté de développement
Habilitation à diriger des recherches, Université Paul Sabatier, octobre 2001.
Abdeldjalil Boudjadar, Jean-Paul Bodeveix, Mamoun Filali
Revising and Extending the Uppaal Communication Mechanism, Springer-Verlag, Vol. 7306, Lecture Notes in Computer Science, juin 2012.
J.-M. Farines, Bernard Berthomieu, Jean-Paul Bodeveix, Pierre Dissaux, Patrick Farail, Mamoun Filali, Pierre Gaufillet, Hicham Hafidi, Jean-Luc Lambert, Pierre Michel, François Vernadat
The Cotre Project: Rigorous Software Development for Real Time Systems in Avionics, COLNARIC, ADAMSKI & WEGRZYN, novembre 2003.
Jean-Paul Bodeveix, Thierry Millan, Christian Percebois, Pierre Bazex, Louis Féraud
NEPTUNE : Method, Checking and documentation generation for UML application
, NEPTUNE Consortium, 2003.
Jean-Paul Bodeveix, Mamoun Filali, Amal Sayah
Programmation en C++, InterEditions, 1994.
Jean-Paul Bodeveix, Christian Percebois, Salam Majoul
Coordinating Objects through Multiset Rewriting
Dans : Special Issues in Object-Oriented Programming, Mühlhäuser, Vol. 3, mars 1997.
Bernard Berthomieu, Jean-Paul Bodeveix, Silvano Dal Zilio, Mamoun Filali, François Vernadat
Vérification formelle de spécifications AADL via FIACRE
Diffusion pédagogique. août 2011.
Jean-Paul Bodeveix, Mamoun Filali, Thomas Polacsek
Projet PAM: AIde à la conception d’une palte-forme avionique
Présentation orale. mars 2009.