Legend has it that Isaac Newton formulated gravitational theory in 1665 or 1666 after watching an apple fall and asking why the apple fell straight down, rather than sideways or even upward. One easy observation gave way to this discovery.
When Archimedes was working on the problem of determining the actual amount of gold in the new crown of King Hieron II of Syracuse, he went to the bathhouse and noticed during the bath that the more he immersed his body in water, the more water in the tub overflowed. When he realized the significance of this observation, he jumped out of the bath and ran home dripping naked shouting Heureka!
Both stories lead us to think that great ideas both come suddenly and unexpectedly. Little do we know how long we have to think and try to solve an issue, before we reach the “eureka” moment.
“The only way to rectify our reasoning is to make them as tangible as those of the Mathematicians, so that we can find our error at a glance, and when there are disputes among persons, we can simply say: Let us calculate [calculemus], without further ado, to see who is right.”
Gottfried Leibniz (1646-1716)
Where Did the Idea Come From?
To understand how we came up with the method of Public Certification of a Specification and its Software that is enabling us to get the most secure software, we must go back in time to 1996. That year, a small Basque legal company, Guretruck, started to see potential business in defending road transport fines, mostly for the calculation of driving times.
In June 1998, the French Ministry of Transport organized four weekends in Bayonna, France, to teach all inspectors how to detect manipulation on the ELD/Tachograph devices. One of the focuses was the process of detecting manipulation of speed limiters (set on 90km/h) that are connected to the tachograph device by a cable. The case Guretruck took was a fine of 15.000 Euro where the cable was cut. For the experts of Guretruck, it was obvious there was a manipulation intent. The cable was cut in one line, leading the experts to believe the cable was cut on purpose. The inspector, who was giving a fine, wrote a processing letter, later used in court. The description he used was “casse” which means “broken”, and not “coupe”, which would mean “cut”.
Guretruck lawyers won the case because they highlighted the word “broken”, which proved that there was no intent of manipulation.
This case showed us how important each word in a natural language of interpretation is.
If the control would be done correctly and the description in the natural language would have been more exact, the result of the defense would have been different. The case lead us to think of the importance of each word in a description. The same goes for defining software. The description of the function of the program and which functions it has/ should have is crucial for the result.
From 1996 until 2006, before the big digitalization of the tachograph happened, the standard was an analog tachograph and the data was saved on paper discs. The paper discs had to be interpreted by the control officers and later were used in legal defense cases as evidence. Discs had printed information about driving that could be interpreted by anyone (officers, judges, lawyers and drivers) just by looking at the disc.
In 2006, after digital tachographs started to be used, the interpretation of digital data saved by the tachograph, could be interpreted only by software made for it. Without the software, saved data makes no sense to anyone.
- Some very clever computer scientists are going to read some very mysterious digital files
- Computer scientists will make all the fine legislations automatic and unable to be interpreted by lawyers anymore.
Guretruck´s team thought it would end the era of possibility of fine defense. The system working properly should provide such clear data, that there is no doubt how to interpret it. Nothing should be interpretable anymore. The law is in the software.
The more the team learned in praxis, the more they saw how badly the regulations were implemented in all software created for Tachograph devices. Depending on the software, the output data was likely to have different results because the final decision of interpreting the law was in the hands of software creators.
They had to use software to see the interpretation of the digital files in order to make a legal defense.
Guretruck contacted a Swiss software creator in 2006 to collaborate. Soon after they realized how many mistakes there were in the interpretation the provided software was creating. The lawyers did not agree with the output of the software file´s interpretation.
The legal team attended multiple conferences and talks with police officers from all over Europe, where multiple interpretations were found. The most crucial was the interpretation of continuous driving time from Article 7.
After a driving period of a four and a half hours a driver shall take an uninterrumpted break of not less than 45minutes, unless he takes a rest period.
This break may be replaced by a break of at least 15 minutes followed by a break of at least 30 minutes each distributed over the period in such a way as to comply with the provisions of the first paragraph.
The two sentences of Article 7 were always interpreted differently by each reader. In consequence, each software had a different version of this regulation with different outcomes.
Guretruck saw the mistakes tried to put attention the mistakes. The idea that a “very intelligent engineer would take the law and make an algorithm”, starts to fail.
Guretruck is a law firm, without any computer experience, but its CEO is a theoretical physicist and was leading this process. Their partnership with the Swiss company began to fail because they were not able to change the algorithms.
Guretruck started hiring software developers then it started to dive into the software creation business.
Guretruck started increasing in computer knowledge frequently the Swiss party generated questions that were uncomfortable.
On July 8th 2008, at 2:00 p.m., the employees of Guretruck were in Turin, Italy, at a checkpoint with the Italian police, training them on the Swiss software, made for interpretation of the digital data, on real examples, to review if a driver was following the rules. They discovered a case that was impossible to explain. Today we call it the “Turin catastrophe”.
Guretruck employees were discussing if there was a malfunction or manipulation of the software. They asked the software creators and the software creators did not know either. The software was showing data from the future, year 2106, and the truck drove 16000000000km with continuous driving of 3 days in a row.
This experience motivated Guretruck to create their own software using their legal perspective as experts on the regulations for tachographs. The software created is used in the majority of European countries as well as in our South American departments.
In 2010, Guretruck released a product called PoliceController, which followed the regulation with such a clear interpretation, that the lawyers had no doubt on its outcomes. Each interpretation done by the software was indisputable. The team wanted to prevent another “casse-coupe” case, so they focused on the details. Since the lawyers collected years of experiences defending cases made by the existing software, and knew its weak points, Guretruck used this knowledge to make better software for data interpretation.
The Regulations are the Technical Specification for the future software. The deep dive into the European regulations made the developer realize the following:
- It is NOT possible to use the regulations as a technical specification without interpretation. You have to make hundreds of decisions that are not written in the law, for the algorithm to work: because the law does not provide for cases that are necessary to develop the algorithm or because the law is inconsistent.
- Another big problem was that laws were written in a natural language to explain how to do mathematical algorithms, and it is impossible to prove, that the algorithm and the text in natural language are the same.
- It was even shown, that in cases where the law is perfectly clear, there are developers who do not comply with it. A very clear example of this is UTC time format. Almost all laws indicate that software must be developed in UTC. No software provider is following this. They are not following this in Europe and neither in North America.
- Guretruck´s made the decision that when it is detected that something is interpretable or inconsistent, a configuration panel should be made for the police to make the decision. Even so, this does not solve the whole problem.
Another remarkable thing was, in 2016, when the Federal Act 395 (as a specification to develop the ELDs), came in force in the United States, Guretruck realized that the definition of “stopped vehicle” was consistent, and produced “unwanted” effects, by not understanding the consequences of the definition. This was already confirmed with 3 years of experience by the FMCSA itself in 2019 through a circular.
Today, we believe that this may be one of the biggest problems that cause “bugs” in software, not really understanding the scope of the specification.
During the software creation, Guretruck ´s team discovered how difficult it is to translate a regulation written in natural language into a code and how easy it is to have bugs and mistakes.
Defining the Goal - Perfect Software
Around 2015, there was a change in philosophy, if Guretruck knew all the bugs that existed in a law before it becomes software, (with the advantage that this lets the legal team win cases in Court), why not try to find a technology, which would make it perfect? Even if it is against the Guretruck core business- for which the fundament were bugs in the software.
They wanted to reach both conditions:
-
A perfect law, mathematically consistent
and without errors, and not interpretable.
-
A law, which would be translated into a
software exactly.
Back then, there was no solution for the above.
Guretruck, by 2015, had already made progress on their goals and had found that there was an algebraic logic between all the driving laws of the USA, Canada, EU, Brazil, Mexico and Chile. Later, it would be called “splitter theory”, but at the time, Guretruck could not move past this point.
In 2015, the CEO of Guretruck, spoke with Universidad de Barcelona´s director of Master in pure and applied logic. After they met a few times, it seemed there was a point in common.
The same year, the University assigned one person to start formalizing Splitter theory. The Splitter theory is a common algebra found to describe, a family of laws of driving times rules for professionals drivers.
The splitter Theory covers:
|
USA |
“Code of Federal Regulations, 49: Transportation, Part 395 Hours of Service Drivers” |
|
CANADA |
“Commercial Vehicle Drivers Hours of Service Regulations (SOR (Statutory Orders and Regulations)/2005-313)” |
|
EU |
REGULATION (EC) No 561/2006 |
|
BRAZIL |
DECRETO-LEI Nº 5.452, DE 1º DE MAIO DE 1943 (Consolidação das Leis do Trabalho). |
|
MEXICO |
NORMA OFICIAL MEXICANA NOM-SCT-2-087-2017 QUE ESTABLECE LOS TIEMPOS DE CONDUCCIÓN Y PAUSAS PARA CONDUCTORES DE LOS SERVICIOS DE AUTOTRANSPORTE FEDERAL. |
|
CHILE |
CÓDIGO DEL TRABAJO |
Then Guretruck started the research:
When Guretruck started the Splitter theory, persons involved in theorizing, us, considered different approaches. First, we did not know that what we were looking for. We thought perhaps it could be called formally verified software. We had the idea of implementing a few algorithms based on some sort of mathematical development to obtain safe and consistent software.
From the very first moment, we realized, that formal verification is a topic that covers different methodologies, so the second challenge was to discover which methodology was the one that best fit our idea for the Splitter theory project.
We went through four different approaches. First, we considered the model-checking approach, but we quickly had the intuition that this method was not capable enough for our project. Second, we thought to use specification language like VDM. This idea was closer to what we wanted, however we considered that it did not have enough tool support, to develop industrial software like the one we had in mind. We also considered working with different theorem provers like Z3 but in the end, we had the same feeling. None of this completely matched the project we had in mind.
Finally, we got into the “proof assistants” field. This seemed to be the solution that we were looking for, but then again, there were different proof assistants based on different mathematical theories and with different properties. Then we discovered a French-proof assistant - Coq. There was a strong community and examples on how to use this proof assistant to develop verified software and then extract this to a functional programming language that could be compiled and executed on any computer. We came across the possibility of using Coq proof assistant in a combination with SSReflect proof language. It was an important semantic to later write technical specification.
After this discovery, we started developing the splitter theory project with a Coq. At the same time, we tried to learn Coq in detail. With this knowledge, a new startup in Barcelona was created. In 2016, Formal vindication SL (Formal V), started and the next year two PhD students joined the project. The goal of Formal vindication SL is the formal verification of the Splitter theory. In 2018, four more interested students joined the group of Formal V to push the project further.
The first years were spent on discovering and exploring the possibilities to find our own path. In the back of our heads, we kept the idea of the possibility to guarantee that the law or technical specification and the final code are the same.
From the Splitter theory which has involved many laws, we’ve reached the idea of: “computable laws“: laws that will be created with the aim to be technical specifications for designing software and automatization of processes through software.
We still worked with the idea that the formal specification in COQ itself should be the law or technical specification, but after years of working on that idea, in 2020, the idea was abandoned. It was deemed simply impossible. The Formal Specification can be understood only by experts in the topic and this by definition cannot be a law to be widely understood.
At that time we discovered that, by the law, UTC standard is a requirement for any time measurement, including all the laws mentioned before for: European tachographs, American ELDs. Microsoft, Apple, and android time managers are still working only in UNIX time. In 2019, we had to stop the Splitter theory development to focus on the development of a Time manager that follows this requirement. Development then urgently we stopped with…
Eureka!
In October 2020, the first public presentation of the FV Time Manager took place. It had to be broadcasted from the University of Barcelona due to the COVID-19 pandemic. Following that date, the team started researching possible ways of to solve the issue that the extraction of Coq programs still carried: going from Coq’s unary representation of natural numbers to OCaml’s binary representation was a nonverified step. In fact, the extraction of natural numbers posed a problem, both because of the risk of overflow and because of the lack of control on the valid inputs, since the OCaml type was cyclic. Thus representing both positive and negative integers, and the Coq type was for unbounded positive integers. A solution was reached thanks to the unsigned primitive integers developed in Coq, and to the signed primitive integers that our team contributed to Coq. This process showed the need of a higher level of certification that makes specifications accessible to users.
In April of the same year, our team developed the concept of Public Certification of a Specification and its Software. Two years later, in April 2022, the first official release of FV Time Manager using the Public Certification method took place. This solution was put under a patent process right away.
This concept has founded the solution for 2 questions:
- How to understand the COQ files, where everything is proved even not understood but in a not formal language.
- To face one of the biggest issues in software bugs: the interpretation of the specifications with all the consequences.
In June 2022, our colleagues from INRIA - National Institute for Research in Digital Science and Technology, confirmed that COQ will have a formally verified extraction into OCAM and C, including primitive integers. We retake again the Splitter theory, what we call “Worldwide Public Certification of Hours of Service of Drivers Laws and their software“
Mid-2023, we expected to have the first Public Certification of a computable law ever, the Public certification of FV Driving time rules (HOS) for professional drivers.
certification of FV Driving time rules (HOS) for professional drivers. We are still growing as a company. At the same time, we are seeking better solutions as our team is growing with more and more people fascinated by this groundbreaking solution and the possibilities it will give to the software creation process.