David Chemouil

David Chemouil - Homepage
Picture of David Chemouil

David Chemouil
Researcher, Computer Science (PhD, habil.)

ONERA DTIS
2 avenue Édouard Belin, 31055  Toulouse, France

Tel: +33 (0) 5 6225 2936
Mail: firstName.lastName@onera.fr

ORCID ORCID iD
								 icon0000-0003-4136-783X

News

  • 07/2018: our paper Analyzing the Fundamental Liveness Property of the Chord Protocol was accepted at FMCAD 2018.
  • 07/2018: our tool paper The Electrum Analyzer: Model Checking Relational First-Order Temporal Specifications was accepted at ASE 2018.
  • 06/2018: PC and organization of FMIS 2018, the 7th International Workshop on Formal Methods for Interactive Systems, affiliated to STAF 2018.
  • 05/2018: Presentation of Electrum at the MIT workshop on the Future of Alloy .
  • 03/2018: our short paper Proposition of an Action Layer for Electrum was accepted at ABZ 2018.
  • 01/2018: The all-new versions of our free-software tools around the Electrum language are released (collaboration with A. Cunha and N. Macedo): cf.  Electrum Analyzer and Electrod repositories

Academic Activities

LINK TO PUBLICATIONS

Research

  • Current topics:
    • Foundational and applied aspects of the Electrum lightweight formal method (an extension of Alloy with LTL that I have co-authored).
    • Formal analysis of protocols, in particular the Chord distributed hashtable (DHT) protocol.
  • Former interests include: isomorphisms of types; formal methods for critical embedded software; multi-agent temporal logic for goal- and agent-oriented requirements modeling.
  • DBLP, HAL.

Service

  • 2018S2-...: member of the Alloy board
  • PC member FM 2019
  • PC member and co-organizer FMIS 2018
  • PC member ABZ 2016
  • PC member CSDM 2010
  • Subreviewer for various conferences and workshops

Advising

Current

  • Jeanne Tawa (PhD student, co-promotor: J. Brunel, advisor: V. Wiels)
  • Thomas Hujsa (post-doctoral student, co-advisor: J. Brunel)
  • External advisor for Chong Liu's PhD (advisors: A. Cunha & N. Macedo, U. Braga)

Past

Collaborative projects

  • FORMEDICIS (ANR), MOISE (IRT Saint-Exupéry), TRUST (FCT, Portugal), IFSE2 (Fondation STAE)
  • Formerly: Topcased (DGE/FUI), SPaCIFY (ANR), Cesar (Artemis), IMAP (DPAC), Merge (ITEA2), Briefcase (RTRA STAE), Cx (DGA & ANR)

Teaching

  • ENSEEIHT: functional programming; free software, software & law
  • Formerly (Univ. Paul Sabatier, ENSEEIHT, ENAC, ISAE/SupAéro): universal algebra and algebraic specification, formal specification, computability theory, language theory and compilation techniques, imperative programming and axiomatic semantics, requirements engineering

Misc

Personal interests

  • Free software
  • Lacan, Freud, Foucault, psychoanalysis, structuralism, epistemology, history of ideas

Short vitæ

  • 2017: habilitation from Université Paul Sabatier
  • 2008-...: computer scientist at ONERA
  • 2004-2008: flight-software architect (Pléiades HR), in charge of R&T on methods and tools for critical-software engineering, and free-software specialist, at the French Space Agency ( CNES)
  • 2000-2004: PhD (on type theory and rewriting) with Sergei Soloviev (advisor) at IRIT, and teaching assistant at Université Paul Sabatier
  • 1999-2000: MSc (on typed actor-based functional programming) with Patrick Sallé, Marc Pantel and Fabien Dagnat at IRIT/ENSEEIHT
  • For fun: my academic genealogy

Academic Publications

[25] Analyzing the Fundamental Liveness Property of the Chord Protocol. J. Tawa, J. Brunel & D. Chemouil. In Formal Methods in Computer-Aided Design (FMCAD). Austin, United States, 2018. [ HAL open archive | model | PDF ]
[24] The Electrum Analyzer: Model Checking Relational First-Order Temporal Specifications. J. Brunel, D. Chemouil, A. Cunha & N. Macedo. In 33rd ACM/IEEE Intl Conf on Automated Software Engineering (ASE). ACM Press, Montpellier, France, 2018. [ DOI | HAL open archive | PDF ]
[23] Proposition of an Action Layer for Electrum. J. Brunel, D. Chemouil, A. Cunha, T. Hujsa, N. Macedo & J. Tawa. In 6th Intl Conf on ASM, Alloy, B, TLA, VDM, Z (ABZ). Southampton, United Kingdom, 2018. [ DOI | HAL open archive | PDF ]
[22] Sur l'assignation de buts comportementaux à des coalitions d'agents. C. Chareton, J. Brunel & D. Chemouil. In Approches Formelles dans l'Assistance au Développement de Logiciels (AFADL). Montpellier, France, 2017. [ HAL open archive | PDF ]
[21] Lightweight Specification and Analysis of Dynamic Systems with Rich Configurations. N. Macedo, J. Brunel, D. Chemouil, A. Cunha & D. Kuperberg. In Proc. ACM SIGSOFT Intl Symp. on the Foundations of Software Engineering (FSE). Seattle, United States, 2016. [ DOI | HAL open archive | PDF ]
[20] On Finite Domains in First-Order Linear Temporal Logic. D. Kuperberg, J. Brunel & D. Chemouil. In 14th Intl Symp on Automated Technology for Verification and Analysis (ATVA). Chiba, Japan, 2016. Long version. [ DOI | HAL open archive | PDF ]
[19] Evaluating the Assignment of Behavioral Goals to Coalitions of Agents. C. Chareton, J. Brunel & D. Chemouil. In Brazilian Symp. on Formal Methods (SBMF). Belo Horizonte, Brazil, 2015. [ DOI | HAL open archive | PDF ]
[18] Safety and Security Assessment of Behavioral Properties Using Alloy. J. Brunel & D. Chemouil. In 2nd Intl workshop on the Integration of Safety and Security Engineering (ISSE). Delft, Netherlands, 2015. [ DOI | HAL open archive | PDF ]
[17] A Logic with Revocable and Refinable Strategies. C. Chareton, J. Brunel & D. Chemouil. Information and Computation (I&C), vol. 242:(2015) pp. 157–182. [ DOI | HAL open archive | PDF ]
[16] A Viewpoint-Based Approach for Formal Safety & Security Assessment of System Architectures. J. Brunel, D. Chemouil, L. Rioux, M. Bakkali & F. Vallée. In Proc. of the 11th Workshop on Model-Driven Engineering, Verification and Validation (MoDeVVa) co-located with 17th Intl Conf. on Model Driven Engineering Languages and Systems (MODELS), vol. 1235. CEUR-WS, 2014. [ HAL open archive | PDF ]
[15] Towards an Updatable Strategy Logic. C. Chareton, J. Brunel & D. Chemouil. In Proc. 1st Intl Workshop on Strategic Reasoning (SR). 2013. [ DOI | HAL open archive ]
[14] Une vue sûreté de fonctionnement pour la vérification d'architectures abstraites. M. Piriquito, P. Bieber, J. Brunel & D. Chemouil. In Conférence francophone sur les architectures logicielles (CAL). 2012. [ HAL open archive | PDF ]
[13] Vers une sémantique des jeux pour un langage d'ingénierie des exigences par buts et agents. C. Chareton, J. Brunel & D. Chemouil. In Approches Formelles dans l'Assistance au Développement de Logiciels (AFADL). 2012. [ HAL open archive | PDF ]
[12] A Formal Treatment of Agents, Goals and Operations Using Alternating-Time Temporal Logic. C. Chareton, J. Brunel & D. Chemouil. In Brazilian Symp. on Formal Methods (SBMF). 2011. [ DOI | HAL open archive | PDF ]
[11] Towards a categorical framework to ensure correct software evolutions. S. Bouveret, J. Brunel, D. Chemouil & F. Dagnat. In HoTSWUp'11 (IEEE 27th Intl Conf. on Data Engineering Workshops). 2011. [ DOI | HAL open archive | PDF ]
[10] An insertion operator preserving infinite reduction sequences. D. Chemouil. Mathematical Structures in Computer Science (MSCS), vol. 18(4). [ DOI | HAL open archive | PDF ]
[9] Modes in Asynchronous Systems. J.-P. Bodeveix, D. Chemouil, M. Filali & D. Thomas. In 13th IEEE Intl Conf. on Engineering of Complex Computer Systems (ICECCS). 2008. [ DOI | HAL open archive ]
[8] A mapping from AADL to Java-RTSJ. J.-P. Bodeveix, R. Cavallero, D. Chemouil, M. Filali & J.-F. Rolland. In Proc. of the 5th Intl workshop on Java technologies for real-time and embedded systems (JTRES). 2007. [ DOI | HAL open archive ]
[7] The AADL behaviour annex – experiments and roadmap. R. Bedin França, J.-P. Bodeveix, D. Chemouil, M. Filali, J.-F. Rolland & D. Thomas. In 12th IEEE Intl Conf. on Engineering of Complex Computer Systems (ICECCS). 2007. [ DOI | HAL open archive ]
[6] TOPCASED Combining Formal Methods with Model-Driven Engineering. N. Pontisso & D. Chemouil. In 21st IEEE/ACM Intl Conf on Automated Software Engineering ASE, pp. 359–360. 2006. Tool demo. [ DOI ]
[5] Isomorphisms of simple inductive types through extensional rewriting. D. Chemouil. Mathematical Structures in Computer Science (MSCS), vol. 15(5). [ DOI | HAL open archive ]
[4] Towards formalising AADL in Proof Assistants. J.-P. Bodeveix, D. Chemouil, M. Filali & M. Strecker. In Proc. of the Second Intl Workshop on Formal Foundations of Embedded Software and Component-based Software Architectures (FESCA), vol. 141. 2005. [ DOI | HAL open archive ]
[3] Non-Standard Reductions and Categorical Models in Typed Lambda-Calculus. F. Barral, D. Chemouil & S. Soloviev. Логические исследования (Logical Investigations), (12):(2005) pp. 300–315. [ PDF ]
[2] Some Algebraic Structures in Lambda-Calculus with Inductive Types. S. Soloviev & D. Chemouil. In Types for Proofs and Programs (TYPES). 2004. [ DOI | HAL open archive ]
[1] Remarks on isomorphisms of simple inductive types. D. Chemouil & S. Soloviev. In Mathematics, Logic and Computation (in honor of N.G. de Bruijn's 85th birthday), satellite event of ICALP, vol. 85. 2003. [ DOI | HAL open archive ]

Keynotes/Lectures

The Design of Spacecraft On-Board Software. D. Chemouil. In Formal Specification and Development in B (Proc . Intl B Conference), page 3, 2007. Invited keynote.

The Design of Space Systems. D. Chemouil. In From MDD concepts to experiments and illustrations, Models driven engineering for distributed real-time embedded systems (MDD4DRES summer school), 2006.

Industrial Publications

Formal Modelling and Safety Analysis of an Avionic Functional Architecture with Alloy. J. Brunel, D. Chemouil, N. Mélédo, and V. Ibanez. In Embedded Real Time Software and Systems (ERTSS), Toulouse, France, 2014.

SPaCIFY: a Formal Model-Driven Engineering for Spacecraft On-Board Software. P. Arberet, J. Bodeveix, F. Boniol, J. Buisson, G. Cannenterre, D. Chemouil, A. Cortier, F. Dagnat, F. Dupont, M. Filali, E. Fleury, G. Garcia, F. Herbreteau, E. Morand, J. Ouy, G. Sutre, A. Rugina, and M. Streker. In Embedded Real Time Software and Systems (ERTSS), 2010.

FDIR Strategy Validation with the B method. D. Sabatier, B. Dellandrea, and D. Chemouil. In Data Systems In Aerospace (DASIA), 2008.

Towards a formal semantics for AADL execution model. J.-F. Rolland, J.-P. Bodeveix, D. Chemouil, M. Filali, and D. Thomas. In Embedded Real-Time Software (ERTS), Toulouse, 2008.

AADL modes for space software. J.-F. Rolland, M. Filali, J.-P. Bodeveix, D. Chemouil, D. Thomas, and A. Rossignol. In Data Systems In Aerospace (DASIA), 2008.

The SPaCIFY Project. D. Chemouil. In Data Systems In Aerospace (DASIA), 2008.

Utilisation d'AADL pour la conception de logiciels de vol satellite. J.-F. Rolland, D. Thomas, and D. Chemouil. Génie Logiciel, 80:41–44, 2007.

Vérification formelle d'un modèle AADL à l'aide de l'outil UPPAAL. N. Pontisso and D. Chemouil. Génie Logiciel, 80:36–40, 2007.

The TOPCASED project-a toolkit in open-source for critical applications and system development. F. Vernadat, C. Percebois, P. Farail, R. Vingerhoeds, A. Rossignol, J. P. Talpin, and D. Chemouil. In Data Systems In Aerospace (DASIA), 2006.

Experimenting an AADL behavioural annex and a verification method. J.-P. Bodeveix, M. Filali, M. Rached, D. Chemouil, and P. Gaufillet. In Data Systems In Aerospace (DASIA), 2006.

Towards the verification of model transformations. J.-P. Bodeveix, D. Chemouil, M. Filali, N. Lalevée, and M. Strecker. In Embedded Real-Time Software (ERTS). Société des Ingénieurs de l'Automobile, 2006.