Skip to Main content Skip to Navigation

Search by documents



...
hal-02332531v1  Conference papers
Jean-Paul BodeveixJulien BrunelDavid ChemouilM Filali. Mechanically Verifying the Fundamental Liveness Property of the Chord Protocol (FM 2019)
3rd 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⟩
...
hal-02382714v1  Journal articles
Fei WangZhibin YangZhi-Qiu HuangCheng-Wei LiuYong Zhou et al.  An Approach to Generate the Traceability Between Restricted Natural Language Requirements and AADL Models
IEEE Transactions on Reliability, Institute of Electrical and Electronics Engineers, 2019, 1 (1), pp.1-20. ⟨10.1109/TR.2019.2936072⟩
hal-03012557v1  Conference papers
Jean-Paul BodeveixJulien BrunelDavid ChemouilM Filali. Mechanically Verifying the Fundamental Liveness Property of the Chord Protocol
Journées du Groupe de Travail Vérification du GDR GPL 2019, GDR GPL (Groupement de Recherche Génie de la Programmation et du Logiciel) - INS2I / CNRS, Jun 2019, Nantes, France
...
hal-02181895v1  Conference papers
Jean-Paul BodeveixArnaud DieumegardM 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
...
hal-01708993v1  Conference papers
Jean-Paul BodeveixArnaud DieumegardM Filali. Pattern-based requirements development
9th European Congress on Embedded Real Time Software and Systems (ERTS 2018), Jan 2018, Toulouse, France
...
hal-01887899v1  Conference papers
Badr SialaJean-Paul BodeveixM FilaliTahar 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
...
hal-01709119v1  Conference papers
Badr SialaTahar BhiriJean-Paul BodeveixM 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
...
hal-01500510v1  Conference papers
Badr SialaMohamed Tahar BhiriJean-Paul BodeveixM 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
hal-03176420v1  Conference papers
Badr SialaTahar BhiriJean-Paul BodeveixM 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
...
hal-01298793v1  Journal articles
Zhibin YangJean-Paul BodeveixM FilaliKai HuYongwang Zhao et al.  Towards a verified compiler prototype for the synchronous language SIGNAL
Frontiers of Computer Science, Springer Verlag, 2016, vol. 10 (n° 1), pp. 37-53. ⟨10.1007/s11704-015-4364-y⟩
...
hal-01153717v1  Journal articles
Zhibin YangKai HuYong-Wang ZhaoDian-Fu MaJean-Paul Bodeveix. Verification of AADL Models with Timed Abstract State Machines
Journal of Software, Science in China Press, 2015, vol. 26 (n° 2), pp. 202-222
...
hal-01150341v1  Conference papers
Zhibin YangJean-Paul BodeveixM Filali. Multi-core Code Generation from Polychronous Programs with Time-Predictable Properties
ACM/IEEE International Conference on Model Driven Engineering Languages and Systems: Workshop on Architecture Centric Virtual Integration - MODELS 2014, Sep 2014, Valencia, Spain. pp. 1-10
hal-01095002v1  Journal articles
Zhibin YangKai HuDianfu MaJean-Paul BodeveixLei Pi et al.  From AADL to timed abstract state machine: a certified model transformation
Journal of Systems and Software, Elsevier, 2014, Journal of Systems and Software, pp.20
...
hal-01226470v1  Conference papers
Elie FaresJean-Paul BodeveixM FilaliManuel Garnacho. An Automatic Technique for Checking the Simulation of Timed Systems
11th International Symposium Automated Technology for Verification and Analysis (ATVA 2013), Oct 2013, Hanoï, Vietnam. pp. 71-86
...
hal-01154264v1  Journal articles
Zhibin YangJean-Paul BodeveixM Filali. A comparative study of two formal semantics of the SIGNAL language
Frontiers of Computer Science, Springer Verlag, 2013, vol. 7 (n° 5), pp. 673-693. ⟨10.1007/s11704-013-3908-2⟩
...
hal-01220607v1  Conference papers
Elie FaresJean-Paul BodeveixM Filali. Event Algebra for Transition Systems Composition - Application to Timed Automata
20th International Symposium on Temporal Representation and Reasoning (TIME 2013), Sep 2013, Penscacolq, FL, United States. pp. 125-132
...
hal-01231769v1  Conference papers
Manuel GarnachoJean-Paul BodeveixM Filali. A Mechanized Semantic Framework for Real-Time Systems
11th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS 2013), Aug 2013, Buenos Aires, Argentina. pp. 106-120
...
hal-01231765v1  Conference papers
Abdeldjalil BoudjadarFrits VaandragerJean-Paul BodeveixM Filali. Extending UPPAAL for the Modeling and Verification of Dynamic Real-Time Systems
5th International Conference on Fundamentals of Software Engineering (FSEN 2013), Apr 2013, Tehran, Iran. pp.111-132
...
hal-00494348v1  Conference papers
Bernard BerthomieuJean-Paul BodeveixSilvano Dal ZilioPierre DissauxM Filali et al.  Formal Verification of AADL models with Fiacre and Tina
ERTSS 2010 - Embedded Real-Time Software and Systems, May 2010, TOULOUSE (31000), France. pp.1-9
...
hal-02267842v1  Conference papers
T CorreaL. B. BeckerJean-Paul BodeveixJ-M FarinesM Filali et al.  Verification Based Development Process for Embedded Systems
ERTS2 2010, Embedded Real Time Software & Systems, May 2010, Toulouse, France. 10p
hal-02061818v1  Book sections
Alexandre CortierLoïc BesnardJean-Paul BodeveixJérémy BuissonFabien Dagnat et al.  Synoptic: a domain-specific modeling language for space on-board application software
Synthesis of embedded software, frameworks and methodologies for correctness by construction, Springer, pp.79 - 119, 2010, Engineering, 978-1-4419-6399-4. ⟨10.1007/978-1-4419-6400-7_3⟩
hal-00788450v1  Conference papers
Alexandre CortierLoïc BesnardJean-Paul BodeveixJérémy BuissonFabien Dagnat et al.  Synoptic: a domain specific modeling language for embedded flight-software
FMA 2009 : Workshop on Formal Methods for Aerospace, Nov 2009, Eindhoven, Netherlands
...
inria-00262442v1  Conference papers
Bernard BerthomieuJean-Paul BodeveixPatrick FarailM FilaliHubert Garavel et al.  Fiacre: an Intermediate Language for Model Verification in the Topcased Environment
4th European Congress ERTS Embedded Real Time Software (ERTS 2008), Jan 2008, Toulouse, France. 8p
hal-00784986v1  Conference papers
Jean-Paul BodeveixDavid ChemouilM FilaliDave Thomas. Modes in Asynchronous Systems
13th IEEE International Conference on Engineering of Complex Computer Systems, 2008, Belfast, Ireland. pp.282 - 287, ⟨10.1109/ICECCS.2008.28⟩
hal-00784968v1  Conference papers
Jean-Paul BodeveixRaphaël CavalleroDavid ChemouilM FilaliJean-François Rolland. A mapping from AADL to Java-RTSJ
5th international workshop on Java technologies for real-time and embedded systems, 2007, Vienne, Austria. pp.165-174, ⟨10.1145/1288940.1288965⟩
hal-00784976v1  Conference papers
Ricardo Bedin FrançaJean-Paul BodeveixDavid ChemouilM FilaliJean-François Rolland et al.  The AADL behaviour annex -- experiments and roadmap
International Conference on Engineering Complex Computer Systems, 2007, Auckland, New Zealand. pp.377-382, ⟨10.1109/ICECCS.2007.41⟩
...
inria-00089493v1  Conference papers
Jean-Paul BodeveixM FilaliJulia LawallGilles Muller. Automatic Verification of Bossa Scheduler Properties
Automatic Verification of Critical Systems, Sep 2006, Nancy, France. pp.19-34
hal-00457182v1  Conference papers
Jean-Paul BodeveixM FilaliJulia LawallGilles Muller. Formal Methods Meet Domain Specific Languages
The 5th International Conference on Integrated Formal Methods, 2005, Eindhoven, The Netherlands, Netherlands. pp.187-206
hal-00784959v1  Conference papers
Jean-Paul BodeveixDavid ChemouilM FilaliMartin Strecker. Towards formalising AADL in Proof Assistants
Formal Foundations of Embedded Software and Component-based Software Architectures 2005, 2005, Edinburgh, United Kingdom. pp.153-169, ⟨10.1016/j.entcs.2005.05.008⟩
hal-00457183v1  Conference papers
Jean-Paul BodeveixM FilaliJulia LawallGilles Muller. Applying the B formal method to the Bossa domain-specific language
The 17th Nordic Workshop on Programming Theory (NWPT'05), 2005, Copenhagen, Denmark, Denmark. pp.35-38