Jean-Raymond Abrial talks to us about the use of B at the RATP (excerpt from his lecture at the Collège de France)/2
They have said, we are going to remove unit tests and remove integration tests,
which is very interesting because the tests for such embedded systems
It's extremely expensive. They removed from the after because the before
was and in October 98, the launch of line 14. Since then, no problem.
Initially, Matra Transports was absolutely against the use of B.
Mr. Hennebert was absolutely incredible. He said, "You're against, okay,
so you're going to do both, one with your techniques and also the
technique with B and then we'll see."
They opened the taps of course and little by little little ones ended up
being convinced and in particular the engineers did very well adapted
to this new technology because it was necessary to prove And in particular
some of these proofs are automatic but others are interactive, i.e. the user
has to use the tool to help the computer to prove. [...] For line 1, what
is remarkable is that for a while there were driverless metros and behind
you had a driver-only metro. I told the RATP that it was very dangerous to
have this because with regard to the automatic system, the metros with drivers
are a kind of mess that you can't control and so it was very difficult.
Why more success? Because Matra Transport has developed a Automatic refinement.
Atelier B developed by the company Clearsy, a tool developed by Matra Transport.
Two companies are doing B, Clearsy and Systerel, and they work very well." [...]
It's extremely expensive. They removed from the after because the before
was and in October 98, the launch of line 14. Since then, no problem.
Initially, Matra Transports was absolutely against the use of B.
Mr. Hennebert was absolutely incredible. He said, "You're against, okay,
so you're going to do both, one with your techniques and also the
technique with B and then we'll see."
They opened the taps of course and little by little little ones ended up
being convinced and in particular the engineers did very well adapted
to this new technology because it was necessary to prove And in particular
some of these proofs are automatic but others are interactive, i.e. the user
has to use the tool to help the computer to prove. [...] For line 1, what
is remarkable is that for a while there were driverless metros and behind
you had a driver-only metro. I told the RATP that it was very dangerous to
have this because with regard to the automatic system, the metros with drivers
are a kind of mess that you can't control and so it was very difficult.
Why more success? Because Matra Transport has developed a Automatic refinement.
Atelier B developed by the company Clearsy, a tool developed by Matra Transport.
Two companies are doing B, Clearsy and Systerel, and they work very well." [...]
Comments
Post a Comment