Julien Brunel

Julien Brunel Homepage

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




  • Julien Brunel, David Chemouil, Alcino Cunha, Thomas Hujsa, Nuno Macedo, Jeanne Tawa. Proposition of an Action Layer for Electrum. In 6th International ABZ Conference ASM, Alloy, B, TLA, VDM, Z, 2018 (ABZ 2018, short paper), Lecture Notes in Computer Science.
  • David Come, Julien Brunel, David Doose. Improving Code Quality in ROS Packages Using a Temporal Extension of First-Order Logic.. In IEEE International Conference on Robotic Computing (IRC 2018), IEEE.


  • Julien Brunel, Peter H. Feiler, Jérôme Hugues, Bruce A. Lewis, Tatiana Prosvirnova, Christel Seguin, Lutz Wrage. Performing Safety Analyses with AADL and AltaRica.In International Symposium on Model-Based Safety and Assessment (IMBSA 2017), Lecture Notes in Computer Science.


  • 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) , 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), ACM Press.


  • 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. 5th Workshop Methods for Modalities (M4M-5) 2007.  Extended version 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. 8th Workshop on Computational Logic in Multi-Agent Systems (CLIMA-VIII) 2007. Extended version in 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