ERTMS Formal Specs: The End of a Long Journey
We hear more about bombastic projects starting than about their successful conclusions (which is understandable: there are far more of the former than of the latter, and people barely brag about how great their failures are. That’s a shame: it would make for a colorful and entertaining read!).
But this post is an exception: it is all about a project that has recently been completed, pursuing a radical vision against quite a few odds.
ERTMS Formal Specs (in short: EFS) is a large scale Domain Specific Language (DSL) project to support the development of a standard-compliant onboard braking systems for trains.
For more information, EFS is described in detail in one of the chapters of my book “The Rise and Fall of Software Recipes”, or on ERTMS Solutions’ website.
EFS is at the crossroads: it is a domain-specific specification language exposing high-level concepts that make sense to the domain experts, but it is also detailed and formal enough to be executable.
EFS is not just a grand plan. It is not just a blue print on flashy slideware. It is now running and complete. It is real. It is robust. And it is a major achievement, in so many ways.
First, stating the obvious, because of completeness: 100% of the specification have been modeled and are now executable in the EFS Scenario Editor. Unlike most efforts around formal specifications, it has not stopped halfway, assuming that someone else would pick it up and complete the project (which never happens, of course. Crossing the T’s and dotting the I’s is nowhere as much fun as making the initial grand plans and demonstrating the approach on a carefully selected subset).
Research projects generally don’t have the stamina and bandwidth to take such ambitious specification projects to completion. Besides, by foregoing executability, all they ever deliver is paper. Allowing for abstractions of various shapes and reach, allowing for unilateral decisions regarding what needs to be modeled vs. what doesn’t, such documentation-producing projects can claim success at more or less any time.
Under the tyranny of quarterly results, commercial organizations do not fare much better. Year after year, budgets must be justified, and the return on investment for such prospective initiatives remains uncertain for a long time.
Which brings me to the second reason that makes EFS a milestone: it is the result of the ruthless pursuit of ERTMS Solutions’ vision, of its way of making software. It was only made possible by the strongest commitment to its beliefs and values, to resist caving in to what most of the industry advocates, even when there was not much new to show for months in a row.
Third, as mentioned above, it is executable. This modeled specification is not a document one can just stare at. It can be animated, and each and every step it takes can be traced back to the part of the specification that justified this behavior. It can be used to produce a production-level implementation by means of a code generator. In a nutshell, it is not just a document that can be used by developers to produce an implementation. It *is* an implementation.
This is all nice and great, but EFS matters to me personally, a lot more than yet another technological step stone.
It may be because I was involved with its inception, even if from a distance (I would not dare claim any credit: helping with some of the initial ideas is dwarfed by the effort it took to bring them to completion).
It may be because the team that has delivered it is close to me, both personally and intellectually.
As a consequence of this closeness it may be because it is a project that I 100% agree with: there is nothing in it I would have done significantly differently.
It may also be because this project was mocked by the crowd of those who could not think outside the box, and could not see value in anything not standard, anything not labeled UML or SysML.
It may be because these crowds have given up ages ago, and have shown to deliver nothing of value. Their failure will of course not prevent these same crowds from applying the same recipes next time, assuming that by learning from their errors, by spending even more time and money, they will eventually prevail, not recognizing how their approach was flawed to start with.
It may be because of its mere size: the EFS formal specification is a huge artefact, even when expressed in a very high level formalism.
It may be because of some combination of these factors, but at the end of the day, it does not really matter.
It is a fantastic achievement.
The ERTMS Solutions team that has delivered the EFS project has made history.
Mark my words.