Julien Brunel

Julien Brunel

Research scientist at ONERA/DTIS

Email: julien(dot)brunel(at)onera.fr

Tel.: +33 5 62 25 26 81

Research interests

  • Logic for computer science
    • temporal / timed logics
    • multi-agent logics
    • model checking
  • Formal approaches to
    • requirements modelling
    • safety analysis of critical systems
    • validation of abstract architecures


See here or DBLP


  • Sofware Validation (with model checking) at ISAE/Supaéro
  • Cyber-physical systems at ISAE/Supaéro
  • Java programming at ISAE/Supaéro
  • Formerly: Java/C/Caml programming, formal specification, language theory (at Université Paul Sabatier and INSA)


Short bio

  • since Oct. 2008 : research scientist at ONERA/DTIM
  • 2008 : post-doctoral research associate at DIKU, University of Copenhagen, Denmark, on the Coccinelle project
  • 2004-2007 : PhD thesis ("Combining Temporal and Deontic Logics for the Specification of Security Policies at IRIT, University of Toulouse with Jean-Paul Bodeveix and Mamoun Filali
  • 2003-2004 : MSc at INPT - ENSEEIH T, Toulouse
  • 2000-2003 : engineer degree in computer science and applied mathematics at ENSEEIHT, Toulouse






  • Denis Kuperberg, Julien Brunel, David Chemouil. On Finite Domains in First-Order Linear Temporal Logic (pdf).In 14th International Symposium on Automated Technology for Verification and Analysis (ATVA 2016) , to appear in Lecture Notes in Computer Science.
  • Nuno Macedo, Julien Brunel, David Chemouil, Alcino Cunha, Denis Kuperberg. Lightweight Specification and Analysis of Dynamic Systems with Rich Configurations (pdf). In 24th ACM SIGSOFT International Symposium on the Foundations of Software Engineering (FSE 2016), to appear.




  • Christophe Chareton, Julien Brunel, David Chemouil. A Logic with Revocable and Refinable Strategies (pdf). Information and Computation, 242:157–182, Elsevier.
  • Julien Brunel, David Chemouil. Safety and Security Assessment of Behavioral Properties Using Alloy. In 2nd International workshop on the Integration of Safety and Security Engineering (ISSE 2015), Lecture Notes in Computer Science.


  • Julien Brunel, David Chemouil, Laurent Rioux, Mohamed Bakkali, Frédérique Vallée. A Viewpoint-Based Approach for Formal Safety & Security Assessment of System Architectures

    In Workshop on Model-Driven Engineering, Verification, and Validation (MoDeVVa 2014)
  • Pierre Bieber, Julien Brunel. From Safety Models to Security Models: Preliminary Lessons Learnt

    In Workshop on the Integration of Safety and Security Engineering (ISSE 2014), Lecture Notes in Computer Science.
  • Julien Brunel, David Chemouil, Vincent Ibanez, Nicolas Mélédo. Formal Modelling and Safety Analysis of an Avionic Functional Architecture with Alloy

    In Embedded Real Time Software and Systems (ERTSS 2014), Toulouse, France


  • Christophe Chareton, Julien Brunel, David Chemouil. Towards an Updatable Strategy Logic

    In Workshop on Strategic Reasoning (SR 2013), Electronic Proceedings in Theoretical Computer Science, 2013.
  • Julia L. Lawall, Julien Brunel, Nicolas Palix, René Rydhof Hansen, Henrik Stuart, Gilles Muller. WYSIWIB: exploiting fine-grained program structure in a scriptable API-usage protocol-finding process

    In Journal of Software: Practice and Experience (SPE), Vol. 43, Issue 1, John Wiley & Sons, Ltd.


  • Julien Brunel, Jacques Cazin. Formal Verification of a Safety Argumentation and Application to a Complex UAV System

    In SAFECOMP Workshops, Lecture Notes in Computer Science, 2012
  • Maria Piriquito, Pierre Bieber, Julien Brunel, David Chemouil. Une vue sureté de fonctionnement pour la vérification d'architectures abstraites

    In Conférence francophone sur les architectures logicielles (CAL 2012), Montpellier, France
  • Christophe Chareton, Julien Brunel, David Chemouil. Vers une sémantique des jeux pour un langage d'ingénierie des exigences par buts et agents

    In Approches Formelles dans l'Assistance au Développement de Logiciels (AFADL 2012), Grenoble, France
  • Pierre Bieber, Julien Brunel, Kushal Gupta, Eric Noulard, Claire Pagetti, Thierry Planche, François Vialard. Reconfigurable IMA platform: from safety assessment to test scenarios on the Scarlett demonstrator

    In Embedded Real Time Software and Systems (ERTSS 2012), Toulouse, France


  • Christophe Chareton, Julien Brunel and David Chemouil. A Formal Treatment of Agetns, Goals and Operations Using Alternating-Time Temporal Logic

    In Brazilian Symposium on Formal Methods, (SBMF 2011), Lecture Notes in Computer Science, 2011
  • Sylvain Bouveret , Julien Brunel, David Chemouil and Fabien Dagnat. Towards a categorical framework to ensure correct software evolutions

    In 3rd Workshop on Hot Topics in Software Upgrades (HotSWUp 2011), Hannover, Germany


  • Pierre Bieber, Julien Brunel, Eric Noulard, Claire Pagetti, Thierry Planche and François Vialard. Preliminary Design of Future Reconfigurable {IMA} Platforms - Safety Assessment

    In 27th International Congress of the Aeronautical Sciences (ICAS 2010), Nice, France


  • Julia L. Lawall, Julien Brunel, Nicolas Palix, René Rydhof Hansen, Henrik Stuart, Gilles Muller. WYSIWIB: A Declarative Approach to Finding Protocols and Bugs in Linux Code

    In 39th Annual IEEE/IFIP International Conference on Dependable Systems and Networks, (DSN 2009), IEEE Computer Society, 2009 (preprint)
  • Julien Brunel, Damien Doligez, René Rydhof Hansen, Julia L. Lawall, Gilles Muller. A Foundation for Flow-Based Program Matching Using Temporal Logic and Model Checking

    In 36th Symposium on Principles of Programming Languages (POPL'09), ACM Press, 2009 (preprint / slides)


  • Philippe Balbiani, Jan Broersen, Julien Brunel. Decision procedures for a deontic logic modeling temporal inheritance of obligations

    extended version of 5th Workshop Methods for Modalities (M4M-5) 2007, in Electronic Notes in Theoretical Computer Science, vol. 231, 2009, (preprint )
  • Julien Brunel, Frédéric Cuppens, Nora Cuppens-Boulahia, Thierry Sans, Jean-Paul Bodeveix, and Mamoun Filali Security Policy Compliance with Violation Management.

    In 5th ACM Workshop on Formal Methods in Security Engineering (FMSE'07), ACM Press, 2007 (preprint / slides)
  • Jan Broersen, Julien Brunel. 'What I fail to do today, I have to do tomorrow', a logical study of the propagation of obligations.

    extended version of 8th Workshop on Computational Logic in Multi-Agent Systems (CLIMA-VIII) 2007, Lecture Notes in Artificial Intelligence 5056, 2008 (preprint / slides)
  • Jan Broersen, Julien Brunel. Preservation of Obligations in a Temporal and Deontic Framework

    In 6th International Joint Conference on Autonomous Agents & Multi Agent Systems (AAMAS-07), ACM Press, 2007



  • Julien Brunel, Jean-Paul Bodeveix, Mamoun Filali. A State/Event temporal deontic logic

    In Eighth International Workshop on Deontic Logic in Computer Science (DEON'06), Lecture Notes in Artificial Intelligence 4048, 2006 (preprint / slides)


  • Julien Brunel, Deontic. Logic for specifying availability policies

    In Proceedings of 6th school on MOdelling and VErifying parallel Processes (MOVEP'04), 2004
  • Julien Brunel. Logique déontique pour la disponibilité

    Master's thesis, Université Paul Sabatier, 2004