UB researchers design bug-free software
Computer programs are playing an increasingly important role in the functioning of society. This dependence also entails exposure to the risks of unavoidable programming errors, which can cause economic losses in the millions, such as those produced by the crash of Boeing 737 MAX prototypes. A team from the University of Barcelona, together with the companies Formal Vindications S.L. and Guretruck S.L., has developed a system to design bug-free software. Using the methods of mathematical logic, this revolutionary technology produces infallible software, achieving an exact correspondence between what the software executes and the instructions it is given. The first result of this project is a formally verified computer time library that provides high-precision time conversions and is to be applied to tachographs, which are vital for the legal regulation of the freight industry.
This project is led by Dr. Joost J. Joosten, a professor of the Department of Philosophy of the UB and a researcher at the Institute of Mathematics of the UB, and has received a grant from the Retos Colaboración call of the Spanish Ministry of Science and Innovation, whose objective is to fund collaborative projects involving companies and research organizations.
Error-free code verified mathematically
Computer programs often need very precise time management to process aspects such as the start time of an event, the deadline of an administrative procedure or the hours that truckers are allowed to drive non-stop. For this process, software relies on time stamps, a digital mechanism that provides evidence that electronic data has been produced at a specific date and time. Errors in the code that manages these dates can have important legal repercussions, such as those caused by defects in the processing of information from a tachograph, the device that controls the driving time slots of truckers.
Within the framework of this project, researchers have developed a time manager to process time data on the basis of a new software library —a subset of resources used for software development— that is formally verified. This library incorporates two new features that make it a high-precision time converter, which makes it ideal for industry sectors that need high standards of security and reliability. First, it has been formally verified to avoid coding errors. The basis of any computer program is the software requirement specification, that is, the detailed description of the actions that the program is supposed to perform. In the new system devised by this project, this specification serves as the basis for the application of an innovative logic-mathematical technique that generates an algorithm translating this specification into mathematical language. To check that it has no errors, it is then formally verified through a demonstration assistant called Coq, a computer program that checks the software’s reliability. “This procedure not only allows us to verify that the code does not contain internal errors, but also demonstrates mathematically that it perfectly matches the specifications,” explains Joost Joosten.
“If someone is sent to jail on the basis of an electronic tachograph reading, it is better to be sure that what the program reports is correct. That’s why infallibility is so important,” Dr Joosten adds.
Software that incorporates leap seconds
The second relevant feature of the new technology is that the calculations of the formally verified software library include leap seconds. These seconds are small discrepancies between atomic time and time measured with respect to the actual rotation of the Earth that are part of the so-called UTC (Coordinated Universal Time or Civil Time) standard, which serves as a reference in most laws dealing with time and durations. However, leap seconds are usually not taken into account in general software libraries, which could lead to errors and legal repercussions. “In a recent publication we have mathematically demonstrated that tachograph logs can be ‘misled’ by ignoring leap seconds to drive from Barcelona to Amsterdam non-stop, which is illegal. In the real world –continues Joosten–this does not usually happen, but deviations in actual driving logs reach around 8%, so with our library we reduce the gap between legal prescription and practical engineering.”
The new time management system is ready to be used not only in the transport sector, but also in any other field that requires time conversions, especially in sectors where an error-free system is most needed, such as aviation, e-commerce, and industry.
This project has a total budget of over EUR 2,200,000 and has been managed through the UB’s Office for the Transfer of Research Results, the FBG. The project, with the file number RTC-2017-6740-7, is co-funded by the European Regional Development Fund (ERDF) of the European Union.