The FV Time Manager
The team has developed a Coq verified library for time conversions between UTC and Unix, including leap seconds [to be published]. More precisely, the Coq Time Library is a verification project consisting of a library for managing conversions between formats of time (UTC and timestamp), as well as some commonly used functions like sums, computation of a duration between two times, etc.
There are of course many libraries to perform conversions between time formats. However, our library incorporates two crucial aspects:
It includes leap seconds. Leap seconds are part of the UTC standard, but they are not usually counted in this kind of general-purpose libraries, because the error is small and irrelevant for many purposes. However, it can be relevant for some, like computations that are meant to enforce a law or regulation, or for critical systems.
It is formally verified, which means that we provide computer-checked mathematical proof that the algorithms to perform time conversions behave exactly according to a simple, human-readable specification.
We introduce a new concept, the formal calendar, to measure time periods. Durations are not well-defined in UTC, because due to leap seconds minutes, hours, etc. do not have constant durations. Our library solves two critical issues by introducing the formal time standard for the time durations in UTC: it gives constant definitions for durations or time intervals, allowing to group durations in units bigger than seconds consistently, and it introduces the functions to deal with time arithmetic consistently when compute time differences, additions and subtractions.
The FV Time Manager is the extraction of these verified algorithms to a computer-efficient language like OCaml, so that it can be used as time manager in industrial projects. Our team can also provide wrappers to other programming languages to facilitate the integration of the manager in developments.