Marc Boyer

Marc Boyer Home page
Marc Boyer
2, av Edouard Belin
31055 TOULOUSE Cedex 4
Tel: (33)

Research area: formal methods for communicating embedded systems

I am working on architectures and formal methods for communicating embedded systems: from theoretical studies on models (Petri nets, network calculus) to practical aspects (architecture, prototype)

I am member of the program committee of ERTS² and I was on the WCTT workshop.

I also sometime contributes to Wikipedia when I am too upset by what is written.

Open positions

There are 3 open PhD positions. Note that the subjects are written in french, but you can of course contact me for details.
  • Avionics and automotive network convergence TIS-DTIS-2018-10 : Avionic industry is currently looking for a successor to AFDX network, whereas automotive industry is looking for a standard real-time Ethernet. Will TSN be the solution? How to compute the guaranteed performances?
  • Co-design of control/command laws and network delays TIS-DTIS-2018-36: Network delays have an impact on the quality of the control of a cyber-physical system. So, currently, the design of a control low model the network as a worst or a mean delay. But with a better model, one can capture the real behaviour of a network. The subject of the PhD is to define and evaluate new kinds of delay model.
  • Network calculus formal proofs TIS-DTIS-2018-07: While real time systems become more complex, the evaluation of their performance also becomes more complex, and so more subject to bugs. One way to get confidence in algorithms is to do formal proofs. The subject of the PhD is to do in Coq proofs of network calculus results.


I teach mainly protocol engineering (specification, V cycle, SDL) in the Telecommunications and Networks department at ENSEEIHT.

I also teach embedded networks at EUROSAE: MIL-STD-1553, ARINC 429/DITS, CAN, ARINC 825, TTP, ARINC 664/AFDX, TTEthernet, SpaceWire, FlexRay...

Publications and talks
For copyright reasons, some papers are not freely downloadable.
Nevetheless, because I am the author, I can always send you a private copy.
So, email me if needed.


[Network calculus]  [Embedded Networks]   [Timed PN]  [Verification of protocols [QoS dynamic renegociation]

Publications related to network calculus

Publications related to embedded networks

  • [MARC12] " Deterministic Execution on Many-Core Platforms application to the SCC", Bruno d'Ausbourg, Marc Boyer, Eric Noulard and Claire Pagetti, Proc of the 4th symposium of the Many-core Applications Research Community, (MARC'11b), Potsdam, Germany, December 2011. <
  • [FET05] "Interconnecting CAN busses via an Ethernet backbone", Jean-Luc Scharbarg, Marc Boyer, Christian Fraboul. Proc of the 16th IFAC International Conference on Fieldbus Systems and their Applications (FeT 2005), Puebla (Mexico), Novembre 2005
  • [ETFA05a] "TTCAN over mixed CAN/Switched Ethernet architecture"; Jean-Luc Scharbarg, Marc Boyer, Jérome Ermont, Christian Fraboul. Proceedings of the 10th IEEE International Conference on Emerging Technologies and Factory Automation (ETFA), Catania, IEEE Computer Press, p. 665-668, septembre 2005.
  • [ETFA05b] "CAN-Ethernet Architectures for Real-Time Applications", Jean-Luc Scharbarg, Marc Boyer, Christian Fraboul. Proceedings of the 10th IEEE International Conference on Emerging Technologies and Factory Automation (ETFA), Catania, IEEE Computer Press, p. 245-252, septembre 2005.

Publications related to verification of protocols

Publications related to timed Petri nets

Publications related to QoS dynamic renegociation


Tools and code


NC-maude have been developped to allow to play with Network Calculus. Current version is 1.9.5. You will need the Maude tool to use it.

You can have a look here to get my feedback on the use of rewriting language in this project.

C++ Code : CheckedNumeric

CheckedNumeric<T> is a C++ class that behaves like a numerical type, but with a checking of overflow and underflow, and throwing of an exception when the results is out of bounds.
Code example:

CheckedNumeric<unsigned int> x,y;
cout<<++x;  // Outputs 2
x=y-1;      // Throw a CheckedNumeric<unsigned int>::numeric_overflow exception

You can download the sources.

C Code : The Basic Preprocessed Library

The Basic Preprocessed Library: this is an attempt of having a set of container and algorithms (like the STL in C++) type-safe and efficient in C, using the preprocessor.
You can browse the documentation: a short user manual and developper manual, and download the sources.
Any feedbacks are welcome!