Proving time properties for the Internet of Things

“At present, execution time is abstract and, in most cases, not yet well integrated into the semantics of computer languages. We have to bear in mind that this time is not part of the logic itself. It's simply a side effect,” reminds Benjamin Lion. However, it is obviously very important. In a factory, imagine a manipulator arm working on a part. The meaning of the program relates to the physical impact that this arm will exert on the part. The machine must take into account not only the logic of the operations, but also side effects such as time. The programmer must therefore have perfect control over time to verify that the part is being handled correctly.”

The same goes for Internet of Things (IoT) and embedded systems. “If the time between two instructions is not well understood, a robot, for example, may have moved before receiving the second instruction. In which case, the second instruction may no longer make sense.”

Giving developers more control

Hence the need to give developers and their programs more control over the preservation of temporal properties. And that's precisely what Benjamin Lion's post-doctorate will be tackling. With two challenges in mind.

The first aims to develop a development framework with sufficient expressiveness to specify the effects of time on programs. But also to provide tools for analyzing the properties of each machine individually, and the resulting global properties for the network as a whole. “Ideally, the design of an application should come as close as possible to the way the developer reasons, so that few errors are made during specification.”

The aim here is to “develop a formal semantics that integrates these time effects and propagates them by composition. If you run one program after another, you want to reason about the time of the whole block as a function of the time of the two parts. At the moment, you can't do this because you don't really understand how time is composed. We're forced to reason about the whole block.”

Benjamin Lion plans to build on “an existing mathematical theory. By using functional semantics with effects, we can model effects in a mathematical structure. I want to instantiate this mathematical theory to propagate time during execution. To my knowledge, this has been done mainly to reason about memory properties, not time properties, although the theory does exist. Most likely, I'll have to amend it in some places.”

Research on the first objective will be carried out in collaboration with Daniel Nowak, researcher at the CNRS. Other scientists involved: Farhad Arbab (CWI Amsterdam) and Hans-Dieter Hiepiep (Leiden University and CWI Amsterdam), as well as Carolyn Talcott (Standford Research Institute). The second challenge concerns the compiler. In other words, the tool responsible for translating the original program into binary code, which the processor then executes.

CompCert compiler.

And that's where CompCert comes in. Designed by Inria^[1], this compiler for mission-critical software has been formally proven. It offers a mathematical guarantee that it generates binary code behaving exactly as prescribed by the semantics of source code written in C language. This tool was proven correct using Coq, a proof assistant also born of research at Inria.

This second part of the research will be carried out with members of Epicure, an Inria^[2] team specializing in formal methods, in which Frédéric Besson who has collaborated with Benjamin Lion on previous projects, works.

UART protocol

Théo Losekoot, a doctoral student who defended his thesis at the end of 2024 with the EPICURE team, popularized his subject around formal proofs as part of the “Ma thèse, une sacrée histoire!” project.

Read his text 

If things go according to plan, Benjamin Lion will then set about generating a certified implementation for UART. “This protocol enables communication between two machines that do not share the same clock frequency. Industry uses it a lot. On an assembly line, for example, there are lots of microcontrollers. But before they can be used, they have to be programmed. During this operation, a crucial step is to write the program to the device's memory. To do this, the developer connects his computer to the microcontroller via a serial cable. Two time-sensitive programs are then run on one of the machines. But if time is not properly controlled, an error may occur during writing. I'd like to certify the accuracy of the time effect of the two programs: to prove that if one runs on the computer and the other on the microcontroller, the latter does indeed behave as desired.”

Un autre cas d’usage porterait sur la vérification formelle de librairies de timers dans les systèmes d’exploitation, en particulier pour RIOT, un système d'exploitation (OS pour operating system) pour l’Internet-des-Objets. “Sur un micro-contrôleur, quand un programme a besoin de connaître le temps, il interroge l’OS qui lui retourne une valeur. Mais peut-on avoir confiance dans cette valeur ? Et d’abord, comment cela fonctionne-t-il ? Et bien en fait, l’OS s’appuie sur deux systèmes. Le premier est un processeur à haute fréquence. Il peut atteindre la micro ou la nanoseconde. Donc très rapide. Mais parfois, il va se décaler dans le temps. Le second est un oscillateur à basse fréquence. Beaucoup plus lent, mais plus précis. Pas de décalage. Un protocole les resynchronise périodiquement. Ce qui génère une source de temps à la fois précise et de haute fréquence. Or, cette resynchronisation, pour l’instant, n’est pas prouvée correcte. Et je voudrais parvenir à le faire.”

Another use case would be the formal verification of timer libraries in operating systems, in particular for RIOT, an operating system (OS) for the Internet of Things. “On a microcontroller, when a program needs to know the time, it queries the OS, which returns a value. But can we trust this value? And how does it work in the first place? Well, the OS relies on two systems. The first is a high-frequency processor. It can reach micro or nanoseconds. So it's very fast. But sometimes, it will shift in time. The second is a low-frequency oscillator. Much slower, but more precise. No time lag. A protocol resynchronizes them periodically. This generates an accurate, high-frequency time source. However, this resynchronization has yet to be proven correct. And I'd like to be able to do it.

Digital factory

Named Cert-t, this project is likely to have an industrial impact by enabling engineers to increase the reliability of time-sensitive applications. Particularly in the field of the Internet of Things (IoT), a sector forecast to double in sales by 2028. It's also worth noting that this post-doctoral work is supervised by Jean-Pierre Talpin. A specialist in time-related issues, this Inria research director is collaborating with Mitsubishi Electric Europe (MERCE). The partnership concerns the certification of cyberphysical properties of critical systems in what are now known as digital factories.

^[1] CompCert's development team received the ACM Software System Award in 2021.

^[2] Epicure is a joint Inria project-team of the University of Rennes, ENS Rennes and CNRS, within the joint research unit Irisa.