Computer programs are becoming more and more important in the functioning of society. This dependency involves one’s exposure to the risk of software errors, which can cause serious consequences in human lives as well as economic losses, such as those that took place when Boeing 737 MAX prototypes crashed.

A team of the University of Barcelona, together with the companies Formal Vindications and Guretruck, has worked on a system to get error-free computer programs. With mathematical logics methods, this revolutionary technology provides an infallible software that reaches an exact correspondence between what it does and the given instructions. The first result of this project is a verified time computer library that enables having high precision time conversions and which is expected to be applied to tachographs, important tools for the legal regulation of the transport industry.

This work is led by Joost Joosten, lecturer at the Department of Philosophy and researcher at the Institute of Mathematics of the UB.

A mathematically verified error-free code
Computer programs need a precise management of time to process aspects such as the start time of an event launch, the dateline of a legal process or the maximum allowed time for shippers. In this process, the software depends on timestamps, the digital mechanism that enables showing electronic data that started at a certain date and time. The errors in the code that manages such dates can have important legal consequences, such as those caused due to the defects in the tachograph data processing, the device that controls time slots for the shippers.

In order to process this time data, researchers have carried out a time manager based on a new software library –a subtype of a computer program used for the development of software– which is verified. Such library provides two new items that turn it into a high precision time converses, excellent for industrial sectors that need security and reliability standards. First, they formally verified it contains no errors in the code, since the base of any computer program is specification, that is, a detailed description of actions we want the program to conduct. The new system uses an innovative logical-mathematical technique to get an algorithm that translates this specification into the mathematical language. Then, in order to check there are no errors, it gets verified through an assistant called Coq, a computer program that tests whether it is completely reliable. “This process allows us to verify the code has no internal errors, and it also shows that the implemented code corresponds to the designed specifications”, notes Joost Joosten. “If the law sends someone to prison, based on a tachograph’s electronic reading, we better be sure that the program says the right thing. This is why such infallibility is important”, adds the researcher.

A program with leap seconds
The second relevant feature of the new technology is that the calculations of the library include leap seconds. These seconds are small discrepancies between the atomic time and the measured time in the Earth’s rotation which is part of the UTC standard (coordinated universal time or civil time), used in most of the laws treating time and duration. However, leap seconds are not usually considered in general libraries, with potential errors and legal consequences. “In a recent publication, we mathematically showed that tachograph records can be mistaken by ignoring leap seconds, and driving from Barcelona to Amsterdam without stopping, an illegal situation. In the real world, —continued the researcher—, this behaviour does not occur, but deviations in real driving records reach up to 8%. With our library we reduce the gap between legal prescription and practical engineering”.

Apart from the transport sector, the new system of time management is available to be used in other fields that need time conversions, specially those sectors that need an error-free code such as aviation, online sales and industry.

This project has a total budget over the 2,200,00 euros and has been managed through the Bosch i Gimpera Foundation, the Office of Research Results Transfer (OTRI) of the UB.

The project, with the file number RTC-2017-6740-7, is co-funded by the European Regional Development Fund (ERDF) of the European Union. Also, it counted on a grant from Collaboration Challenges by the Spanish Ministry of Science and Innovation, whose aim is to fund projects in collaboration with companies and research organisms.