Daniel Fredholm, författare på Prover - Engineering a Safer World

Formal verification – why and how?

Daniel Fredholm — Wed, 24 Jan 2024 13:30:01 +0000

RECORDED WEBINAR

daniel.fredholm

Recorded on March 6, 2024

When commissioning a rail control system, it goes without saying that establishing safety, that the system does not allow any unsafe behavior, is one of the most important activities. That activity can be thought of being made up of three stages:

1. Establish a complete set of safety requirements, or signaling principles
2. Implement the system using those requirements.
3. Verify that the implemented system fulfills the requirements.

In this webinar, we will focus on step 3, the verification step. The traditional methods for safety verification are combinations of testing and manual review. We will talk about formal verification, a verification method that uses mathematical proofs to establish that the implemented system fulfills the safety requirements.

Agenda:

What is formal verification
How is formal verification done
How does formal verification compare to traditional verification methods
Recommendations and considerations for using formal verification

Yes please, send me the recording!

Hosts

Daniel Fredholm
Senior Consultant, Prover

Sara El Mennaoui
Formal Methods Expert, Prover

Inlägget Formal verification – why and how? dök först upp på Prover - Engineering a Safer World.

Why formal verification

Daniel Fredholm — Wed, 15 May 2019 14:37:41 +0000

RECORDED WEBINAR

daniel.fredholm

The only solution to safety verification

Safety verification is vital for interlockings. During this webinar we will describe the general problem of safety verification and show that formal verification is the only method that provides 100% coverage when verifying safety requirements.

Agenda:

The state space explosion
Why traditional verification methods are inadequate
Why formal verification provides a solution

Yes please, send me the recording!

Hosts

Daniel Fredholm
Senior Consultant, Prover

Inlägget Why formal verification dök först upp på Prover - Engineering a Safer World.

Why formal verification – The solution to the verification problem (part 3/3)

Daniel Fredholm — Mon, 24 Feb 2020 06:57:19 +0000

If you have read the first two parts of this series (Read Part 1 here and Part 2 here), then you know that verifying an interlocking that satisfies safety requirements is not an easy task to accomplish. Due to the huge size of the state space of the interlocking, neither manual methods nor testing will get you all the way. You also know that mathematics is the place to look for methods that will. So finally we can start talking about formal verification.

As usual in science, in order to transfer the verification problem into the realms of mathematics, we make mathematical models of the parts involved: the interlocking and the safety requirements. The part of mathematics that can provide us with suitable methods and concepts is logic. What we want to know are things like the following:

When the interlocking commands a signal to show proceed, is there a locked route that begins at that signal?

We want to provide convincing, airtight, arguments showing that such statements are true; i.e. we want a proof of this. Mathematical logic is exactly the part of mathematics that can provide us with an answer. There, things like ‘truth’, ‘statement’, and ‘proof’ are given a precise meaning. The core of the matter is to make mathematics of this kind of question:

Does the truth of statement A force the truth of statement B?
Or, which luckily amounts to the same thing,
Is there a proof of statement B from statement A?

And that is exactly the kind of mathematics we need to solve the verification problem.

In formal verification, what we do is build a logical model of the interlocking – our statement A – and another model of the safety requirements – our statement B. Hence, we have managed to transform the verification problem into a mathematical problem, which means that if we are able to produce a proof of statement B from statement A, we have actually proved that the interlocking satisfies the safety requirements. We have proved that the interlocking will never enter a state where the safety requirements are violated.

So in theory, all is well. Does it work in practice?

Fortunately, it does work in practice as well. The reason is that the most important tasks can be done by computer tools. In particular, there are computer tools that can find a proof of statement B from statement A. When it comes to the modeling parts, the biggest one is the modeling of the interlocking. But also this task can be done by computer tools similar to a compiler, translating the interlocking program into a logical model while preserving all important aspects of the original program. The modeling of the requirements is usually done by hand, but that can be done in a generic part and a specific part. These are then feed into the proving tool which specializes the generic requirements to the particular interlocking that is to be verified. Thus, the generic requirements can then be reused for other interlockings, which minimizes the time spent on modeling the requirements.

This blog concludes this series of blogs answering why formal verification is the solution to the verification problem. I hope you are convinced. Or are at least curious.

Inlägget Why formal verification – The solution to the verification problem (part 3/3) dök först upp på Prover - Engineering a Safer World.

Why formal verification – The suitability of formal verification (part 2/3)

Daniel Fredholm — Mon, 17 Feb 2020 06:45:35 +0000

Hopefully you have read part 1 on this blog, where I tried to convince you that traditional methods will not get you very far when verifying safety requirements for railway interlockings.

This time my task is to convince you that formal verification will get you far. In fact, all the way.

So what is formal verification?

Well, we already know what verification means. The ‘formal’ part means ‘mathematical’. Thus, formal verification means that the verification problem is made into a mathematical problem. And since we enter the realm of mathematics, all the rigour and precision that comes with mathematics are available to us.

The typical activity in mathematics is to make statements and then prove that they are true. Sounds familiar? And the proof of a mathematical statement has to be so convincing, so airtight, that any person with the proper education should agree that the statement actually is true. Of course, in practice the last part can be hard to achieve. Some parts of mathematics are notoriously difficult to understand even with a proper education. But let’s consider a classic example from arithmetic. The statement I am thinking about is as follows:

1 + 2 + … + n = n(n+1)/2.

In my mind, the most elegant way to prove this goes as follows. Write down the sum on the lefthand side twice, one under the other.

1 + 2 + … + n
n + (n-1) + … + 1

Note that the order of the terms is reversed in the lower sum. Now here comes the trick: if we look at the columns in this expression, each column has the sum n+1. And there are n columns. Hence, the sum of all these numbers is n(n+1). What we have then is

2(1 + 2 + … + n) = n(n+1),

which means that

1 + 2 + … + n = n(n+1)/2.

Isn’t that a convincing argumentation?

With this example, I have tried to show you how a mathematical proof can be done and hopefully you agree that, when properly done, mathematical proofs are airtight. In fact, they are the only airtight form of proofs known. As we noted in part 1, the major snag with the verification problem is the huge size of the potential state space. Mathematics provides solutions to this as well, since all domains handled are huge, often infinite.

It turns out that I only got halfway through my aspiration to convince you about the suitability of formal verification. So please wait until the next post.

Inlägget Why formal verification – The suitability of formal verification (part 2/3) dök först upp på Prover - Engineering a Safer World.

Why formal verification – Verifying safety requirements on railway systems (part 1/3)

Daniel Fredholm — Mon, 10 Feb 2020 06:16:54 +0000

The subject I am going to write about this time is not an easy one. I will try to explain why formal verification is good. In particular, why it is a good practice to use formal verification when verifying safety requirements on railway systems.

The verification problem

In order to make a convincing argument, I need to start from the beginning. It all begins with a system and some safety requirements that the system is supposed to satisfy. Let’s assume that the system is an interlocking. Now, the general problem is to provide a convincing argument proving that the interlocking actually fulfills the safety requirements; this can be called the *verification problem*.

Let’s think a bit about the verification problem. What is it that needs to be done? What we have is interlocking software and some safety requirements. In order to make things clearer, let’s assume that the software consists of a number of boolean variables. Some of these variables are inputs, some outputs, and some (probably the most) are internal or intermediate variables. An assignment of values to the variables then represents a potential state of the interlocking. And the collection of all such assignments represents the potential state space. Potential states are related by the interlocking in the sense that one potential state can be reached from another by executing the interlocking for one or more cycles. Also, some of the potential states correspond to assignments that occur during start-up. These are called initial states. Then the reachable states are the part of the potential state space that can be reached from the initial states. Most likely, this is just a small part of the potential state space.

What is a safety requirement?

In the context of the potential state space, what is a safety requirement? Well, a safety requirement is an event that is not supposed to happen. In the end, a safety requirement is one or several assignments of variables that the interlocking should not be able to realise. Hence, a safety requirement is a part of the potential state space that the interlocking never should reach. So the verification problem boils down to showing in a convincing way that the parts of the potential state space that represents the safety requirements does not contain any states that are reachable by the interlocking.

That doesn’t seem so hard does it?

Well, actually it is.

And the main reason is that the potential state space is huge.

In fact, if we only consider boolean variables,
this space contains 2^{number of variables} potential states.

If the interlocking contains 100 boolean variables, then the potential state space has
1 267 650 600 228 229 401 496 703 205 376 ~ 10^30 members!

As a comparison, the number of trees on Earth is estimated to be 3*10^12. And that is just for 100 variables, which would represent a very small interlocking.

It should be clear by now that no manual method can completely solve the verification problem. Also testing fails. To obtain full coverage with testing, one has to try all possible combinations of values of the input variables and then simulate the system in order to verify that no safety requirements are violated. But even with just a small number of input variables this is not feasible. If the number of input variables is 100, then to complete the testing in 1 year would require 4*10^22 test cases to be completed in each second.

So what is a solution to the verification problem?

I think you can guess…

Inlägget Why formal verification – Verifying safety requirements on railway systems (part 1/3) dök först upp på Prover - Engineering a Safer World.

Performance issues with formal verification

Daniel Fredholm — Tue, 17 Apr 2018 08:24:16 +0000

We’ve all been there, waiting for the theorem prover to answer. Getting up for a cup of coffee, bugging a colleague… still no answer. This can be standard behaviour when doing formal verification. The requirements are difficult to prove, the system manages to escape into some dark corner not easily approached by the theorem prover. If things are really bad, then the waiting might continue for hours, days, even weeks!

More is not better

The common remedy for this condition is to get more computers, more powerful computers, more memory, parallel computers, more, more… more usually helps to solve the current situation. But soon another larger system comes along and the condition returns. What I am saying is that, usually, perfomance issues when doing formal verification are a symptom of a more serious disease. And trying to cure it with more computer power is like treating cancer with stronger painkillers; it only addresses the symptom, not the cause.

System disharmony

In my experience, the cause of performance issues when doing formal verification is not lack of computer power. It is rather an indication that the requirements and the system verified are not in harmony. With this, I mean that the system might satisfy the requirements, but not in an obvious way. If the requirements are satisfied, then they are done so in some roundabout, tricky way, not by some straightforward checks, making them hard to prove.

The root cause of this disharmony is usually that the system was not developed for verification, causing the fulfillment of the requirements to be addressed late in the development process. The obvious cure is prophylax. Ideally, the requirements should be available at the beginning of the development of the system. Then the developers can design the system so that it satisfies the requirements in an obvious way. This will make the requirements easy to prove and all performance issues go away. Furthermore, formal verification should be introduced as early as possible in the process so the developers have a chance to confirm that they are on the right track.

In case you are wondering, this is how development is done in the Prover Trident process.

Inlägget Performance issues with formal verification dök först upp på Prover - Engineering a Safer World.

The structure of specifications

Daniel Fredholm — Wed, 11 Apr 2018 08:18:31 +0000

In my last post I wrote about how to write a decent specification on a quite general level. This time, I like to return to the topic, trying to be a bit more specific and tell you something about how we at Prover like to do things. In the Prover Trident Process, the specification of an interlocking is done in four parts: the object model, the generic design specification, the generic safety specification and the generic test specification.

Specifying interlocking software

What is it one needs to specify when specifying interlocking software? Basically, a specification should answer two questions: what and how. The ‘what’ part should tell you what the interlocking should do. In order words, it should specify expected behaviour. The ‘how’ part should tell how this expected behaviour is to be accomplished.

The ‘what’ part – What the interlocking should do

Let’s begin by looking at the ‘what’ part. As we already noted, this is to tell us something about the expected behaviour of the interlocking. To put it simply, the interlocking is expected to allow trains to run in a safe way. If we look closer on this simple statement, we see that it actually contains two parts. The interlocking should allow some things (‘trains to run’) while prohibiting other things (‘in a safe way’). In terms of functionality, it thus makes sense to talk about positive functionality, the things allowed, and negative functionality, the things prohibited.

How does one specify positive functionality? This is nothing else than test cases. For example, if a route fulfills all the requirements for locking and clearing the signal at the beginning of the route, then a request of the route should result in the locking of the route and clearing of the signal. All these test cases are collected in the generic test specification.

What about negative functionality, the things prohibited? Since this is supposed to describe things that are never to happen, it is not practically possible to specify these as test cases. Instead, they are to be thought of as requirements. And since they are to ensure safety, they are actually safety requirements. A typical example could be the following: ‘If a route is locked, then all track circuits that are part of the route should be free of obstacles’. The safety requirements are written down in the generic safety specification.

The ‘how’ part – How the interlocking is to function

With the generic test specification and the generic safety specification, we now have a complete answer to the ‘what’ part of the interlocking specification. What remains is the ‘how’ part. This is done in the generic design specification. It should tell us how the interlocking is to function; how are routes to be locked, signals cleared, switches thrown and the like. In other words, the generic design specification is an implementation of all the functions that are to be present in the interlocking.

So are we done now? Well, not quite. The generic test and safety specifications tells us the expected behaviour of the interlocking, whereas the generic design specification gives an implementation of the interlocking. Hence, they all are supposed to refer to the same thing. The question that remains to be answered is how do we ensure that they do that. Consider route locking, for instance. How do we make sure that the route locking in the generic test specification, the generic safety specification and the generic design specification are all the same? This is where the object model comes into play.

The object model

The object model specifies the types of objects that are present in the interlocking. These can be concrete, representing real railyard objects like track circuits, signals, and switches. They can also be abstract, like routes and local release areas. For each object type, the object model specifies a number of things. The exact list may vary, but it typically includes inputs (which may be categorized into physical inputs and inputs from office system); important states, like ‘locked’ for routes; and outputs, including physical outputs. The main thing is that the object model provides sufficiently rich points of reference to the interlocking so that the other specifications can be written without any further data. It specifies the common concepts of the other specifications.

Although I mentioned the object model last, it is actually the part that should be developed first. Then the generic design, test and safety specifications can be developed independently and in parallel.

How safe and efficient are your rail control systems? Let’s find out!

Inlägget The structure of specifications dök först upp på Prover - Engineering a Safer World.

How to write a decent spec

Daniel Fredholm — Tue, 27 Mar 2018 09:38:31 +0000

Anyone who has given it a go knows that writing specifications is hard work. In fact, at times it seems almost impossible. Which probably is the reason why the practice of using specifications is shunned and dodged whenever possible. Which is bad.

However, if one finds oneself working in the field of railway interlockings, they cannot be avoided. Which is good. So why is it hard to write a good one? And how do you do it?

To me, the main difficulty in writing a good specification is choosing an appropriate level of detail. Let me explain what I mean with this. Software development is a journey from fluffy abstract ideas (‘it should be safe’) to gritty concrete code (‘ExtIsRed := if …’), with the ambition that some of that fluffyness is actually captured in the final code; not an easy task. The fact that the person with the fluffy abstract ideas is usually not the same as the one who writes the code does in no way make this easier. In fact, these persons serve very different purposes in the development process, one making demands and the other one implementing a software product that has to meet these demands. This is where the specification enters the picture. The specification serves as the bridge, or the interface, between the two.

At this stage, perhaps the point I was trying to make becomes a bit clearer. Since the specification serves as a bridge between the user and the implementer, it has to fulfill two purposes; it has to be understood by two parties, and those parties can be quite different sorts of characters regarding education, skills, ways of expression and even personalities. The specification should be detailed enough so that demands and requirements are expressed in a clear and understandable way, but also not too detailed in order to leave some space of manoeuvring to the implementer.

If it is so hard writing good specifications, is it even worth trying? the reader may ask. Well, if one has any ambition at all concerning user satisfaction, or following safety regulations, then the answer to the second question is yes. In fact, as pointed out earlier, specifications are often mandatory when developing safety-critical systems.

So how is this seemingly impossible act accomplished? As with most things, writing good specifications is a question of the right people employing a proper method. With the right people I mean people who can serve as the bridge between users and implementers. This means that they should be very well acquainted with the domain, preferably experts, but also have a fair idea of how the specification will be used. When it comes to safety-critical systems such as interlockings, the specification will first serve as input for the implementation; then it will be used as grounds for verification. The implication is that the requirements formulated in the specification should not only be clear and understandable, they should also be verifiable.

As a choice of method, I would go for some kind of formalism, given my habits. However, this is not for everyone. In general, it might be a better way to write the specification in natural language, but with a rigour and precision inspired by formal systems. This includes giving careful descriptions of all the different types of objects mentioned by the requirements. It also includes giving proper definitions of all the particular notions and relations that relate these objects to each other. Having laid such a foundation, the actual requirements can then be written in the clear, understandable and verifiable way we long for.

In the end, never aim for a perfect spec. A decent one will do.

Text and Photo: Daniel Fredholm

Inlägget How to write a decent spec dök först upp på Prover - Engineering a Safer World.

Railway market in China is a new mission for Prover

Daniel Fredholm — Wed, 13 Dec 2017 09:02:43 +0000

Prover recently started its first project in China, so in the beginning of December Prover did a tour to China, starting in Shanghai, in order to further explore the Chinese interlocking market. The railway market in China represents a huge opportunity, (as it plans to massively expand the railway network), and at the same time some major challenges.

The team from Prover consisted of Fei Niu, myself and our CEO Anders Lindén. Chongjun, our Chinese partner, offered us invaluable assistance with all arrangements: arranging meetings, letting us use their wonderful office and in general took very good care of us.

We visited several cities and had the opportunity to meet some of the major players in the Chinese Railway and Interlocking market and we did some really interesting observations.

Railway market in China is developing fast

With the risk of stating the obvious, the first thing that stroke was the immensity of the Chinese market. For a European, this is almost unfathomable. For instance, in Shanghai, there are well established plans of building 30 new metro lines within the next 5-6 years! This has the implication that Chinese interlocking providers work under much higher pressure regarding delivery schedules and the like than one encounters in Europe.

Also, the level of competence of the Chinese providers seems to be very high. Everybody we met had a firm grasp of both the general principles and the particulars concerning not only interlocking but also computer science.

Finally, we also noted a genuine interest in the products and services that Prover can provide when it comes to Interlocking Design Automation. Chinese companies seems to be driven by a humble pragmatism, not letting pride or ego get in the way of adopting something useful. With safety first, fast and cost efficient delivery of interlocking systems are crucial to them.

All in all, our general impression is very positive. The railway market in China seeems close to ideal for applying interlocking design automation ideas and we look forward to more interesting and succesful cooperations in the future.

Inlägget Railway market in China is a new mission for Prover dök först upp på Prover - Engineering a Safer World.