‘Software Fallo 0′, a UB project to create an error-free software system
All software contains bugs; even the software that controls the aeronautical or military industry has bugs in its final version. This situation is particularly troubling because of the increasing dependence on software of key processes such as computer voting mechanisms, medical technologies, and applications that decide whether or not a person complies with the law. A team from the University of Barcelona participates in a four-year project that promotes a new paradigm for the software industry: the development, for the first time in Spain, of error-free large-scale software. The project ‘Software Fallo 0’ will apply an innovative coding methodology to evaluate the data collected by tachographs, instruments that monitor the activity of vehicles to detect non-compliance. Currently an unverified software application performs this task and, like any software, it makes mistakes that have caused great losses to companies in the sector, and even serious damage to people’s rights.
“The method for producing this error-free software involves not only an abysmal change in the quality of the final product, but also a change in the coding paradigm, since traditional coding uses a type of architecture that is responsible for a large part of the errors or bugs,” explains Joost Joosten, a professor at the Department of Philosophy of the UB and researcher at the Institute of Mathematics at the UB who leads the project. “The average number of errors per thousand lines of code in the software industry is usually between 15 and 50. Formally verified software guarantees zero bugs,” recalls this researcher.
A product for the European Union, the United States, Brazil, and Canada
The first phase of the project is the creation of a piece of software capable of reproducing the regulations for road freight transport on the basis of the transport regulations of the European Union, the United States, Brazil, and Canada, all of which currently have the same technological problem in this field. The methodology to achieve this objective consists in writing formal specifications, in this case based on transport laws, instead of writing the software directly, and translating these specifications into a logical-mathematical language from which the definitive software can be extracted without errors.
“Through this process, a computer program is directly obtained that guarantees compliance with specifications based on the law. The key difference is that this code is derived from mathematical demonstrations. These demonstrations ensure 100% correctness of the code with respect to the specifications outlined at the beginning of the process,” explains Joost Joosten.
Software verified by means of logical-mathematical demonstrations
This methodology is based on the functional programming paradigm, which is often used in sectors where reliability is critical. Subsequently, the goal is to take the security standard one step further and turn the program into a formally verified and therefore error-free code certified by a logical-mathematical process. “The main difference between formally verified software and traditional software is that the latter is tested only on particular cases, in a process that is carried out following the development of the program. In contrast, formal verification aims to verify the total set of possible executions of the program. For this reason, the procedure by which any software is formally verified is totally different, since it must be accompanied by the strength of mathematical demonstrations. In fact, the resulting code is the product of these demonstrations, and is therefore tested beforehand,” notes Joosten.
Formal verification has recently aroused the interest of NASA, which will soon carry out its 11th Symposium on Formal Methods, and has already been implemented in other projects. One of the first such projects was the Paris Driverless Metro, RATP. Their reports indicate that the formal verification of the software revealed errors that the intensive testing phases had not revealed. However, with respect to the methodology used in Paris, the methodology of this project, which uses a demonstration assistant called Coq, is more ambitious, because it is more demanding but at the same time more powerful, that is, it is capable of taking formal verification to more complex areas. Some successful projects using this same methodology are CompCert, a C programming language compiler formally verified using Coq, and the eChronos RTOS operating system, formally verified using the Isabelle proof assistant.
The theory of advanced demonstration, which is a branch of mathematical logic, underlies all these techniques. “We demonstrate mathematically, using a logic called constructive logic, that there is an algorithm with this or that other property, in this case the specifications obtained from transport regulations. Thus, the extracted algorithm will be accompanied by a certificate accrediting that it meets the specifications. This certification process is long, but all the steps needed to complete it are very simple and the correction can be verified with Coq, a program that serves as a proof assistant. The many but simple steps that confirm that the software is correct are therefore verified in advance,” summarizes Joost Joosten.
Less bureaucracy and less erroneous sanctions
The result of the project will mean a great advance. Since it will not make errors, it will eliminate the possibility of erroneous sanctions due to bugs in the software that evaluates tachograph data, which will in turn reduce administrative and judicial processes and generate legal security for both transport professionals and law enforcement agencies.
This initiative, which has a total budget of over €2,200,000, falls under the Retos Colaboración call of the Spanish Ministry of Science and Innovation and Universities, whose aim is to fund collaborative projects between companies and research organizations. In addition to the FBG of the University of Barcelona, the project consortium also includes Guretruck, a company that offers computer and legal engineering services related to the transport sector, and Formal Vindications, a company specialized in the formal verification of technical specifications and software.
