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

• Formal specification and verification (see the Electrum language)
• Temporal logic, model checking
• Formal approaches to the validation of software, architectures and distributed systems

Publications

See here or DBLP

Teaching

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

Short bio

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

Publications

• Quentin Peyras, Julien Brunel, David Chemouil.
  Sound Verification Procedures for Temporal Properties of Infinite-State Systems. In 33rd International Conference on Computer-Aided Verification (CAV 2021), Lecture Notes in Computer Science. [ pdf ]
• Quentin Peyras, Julien Brunel, David Chemouil.
  A Decidable and Expressive Fragment of Many-Sorted First-Order Linear Temporal Logic. In Information and Computation, Vol. 280, Elsevier. [ pdf ]

• Nathanael Sensfelder, Julien Brunel, Claire Pagetti.
  On How to Identify Cache Coherence: Case of the NXP QorIQ T4240. In 32nd Euromicro Conference on Real-Time Systems (ECRTS 2020), LIPIcs. [ pdf ]

• Quentin Peyras, Julien Brunel, David Chemouil.
  A Bounded Domain Property for an Expressive Fragment of First-Order Linear Temporal Logic. In 26th International Symposium on Temporal Representation and Reasoning (TIME 2019), LIPIcs. [ pdf ]
• Jean-Paul Bodeveix, Julien Brunel, David Chemouil, Mamoun Filali.
  Mechanically Verifying the Fundamental Liveness Property of the Chord Protocol. In 3rd World Congress on Formal Methods (FM 2019), Lecture Notes in Computer Science. [ pdf ]
• Nathanaël Sensfelder, Julien Brunel, Claire Pagetti.
  Modeling Cache Coherence to Expose Interference. In 31st Euromicro Conference on Real-Time Systems (ECRTS 2019), LIPIcs. [ pdf ]
• Julien Brunel, David Chemouil, Alcino Cunha, Nuno Macedo.
  Simulation under Arbitrary Temporal Logic Constraints. In 31st Euromicro Conference on Real-Time Systems (F-IDE@FM 2019), Lecture Notes in Computer Science. [ pdf ]

• Julien Brunel, David Chemouil, Jeanne Tawa.
  Analyzing the Fundamental Liveness Property of the Chord Protocol. In 18th Conference on Formal Methods in Computer-Aided Design (FMCAD 2018), IEEE Press. [ pdf ]
• Julien Brunel, David Chemouil, Alcino Cunha, Nuno Macedo.
  The Electrum Analyzer: model checking relational first-order temporal specifications. In 33rd International Conference on Automated Software Engineering (ASE 2018), IEEE Press. [ pdf ]
• 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 (ABZ 2018, short paper), Lecture Notes in Computer Science. [ pdf ]
• 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 Press. [ pdf ]
• David Come, Julien Brunel, David Doose.
  Source Code Analysis with a Temporal Extension of First-Order Logic. In Formal Methods: Foundations and Applications, 21st Brazilian Symposium (SBMF 2018), Lecture Notes in Computer Science. [ pdf ]

• 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. [ pdf ]

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

• Christophe Chareton, Julien Brunel, David Chemouil.
  A Logic with Revocable and Refinable Strategies. In Information and Computation, Vol. 242, Elsevier. [ pdf ]
• 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. [ pdf ]

• 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). [ pdf ]
• 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. [ pdf ]
• 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.
• 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
• 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 Agents, Goals and Operations Using Alternating-Time Temporal Logic. In Brazilian Symposium on Formal Methods, (SBMF 2011), Lecture Notes in Computer Science
• 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 [ 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 (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 [ 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 [ preprint ]
• 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 [ preprint ]
• 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

• 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 [ preprint ]

• Julien Brunel.
  Logique déontique pour la disponibilité. Master's thesis, Université Paul Sabatier, 2004