Re: Certification of Tools/Components

Re: Certification of Tools/Components

From: Nancy Leveson <leveson_at_xxxxxx>
Date: Thu, 06 Aug 2009 10:50:21 -0400
Message-Id: <200908061450.n76EoLR23998@xxxxxx>
Yes, people are using these things. Much of the use is in
hardware (which has some properties that make the use of
tools like model checkers easier). But the question is HOW
are they using them. I'm most familiar with TCAS. There 
have been claims to have model checked it. But they could
only check the boolean logic parts of it, which were the
simplest and no errors were ever found in that part. The
hardest (and biggest) part is the algorithms to determine
whether an aircraft is a threat. That's where all the problems
were found. Those parts could not be model checked because
they contain complex mathematics, so they simply simulated
them. An executable specification language can do that. 

That group also came to me and asked me what they should
model check. I told them that was what they were supposed
to decide. In the end, they found only two errors in the
spec they made (which was from our original spec) which
had been found easily by the human reviewers. They did not
find any of the subtle ones not found by the humans (during
the original V&V) that were not found until operational use.

So, again, yes people are using these tools. The question is
how well they are using them. I remember seeing some supposed
formal specifications during the period when the British MOD
still required them. They were nonsense.


      I have been working in the field of formal specification and
      formal analysis of systems for a quarter century now. These complaints
      about "formal methods" could well have been written back then.
      People don't like Z. You need a PhD to understand how to use a  
      language. You can do things in a language readable with 10 minutes'  
      and it's just as good as formal notations. Logic is too hard for  
      Engineers have no time to understand computer science. There is no  
      motivation for using formality. And so on.
      Meanwhile, SPIN has turned from a one-man research project into a tool  
      used by
      thousands, indeed you can't design telecommunications protocols any  
      more without
      someone insisting you model-check them. Cadence has a very successful  
      business built
      on temporal-logic model checking, Lockheed Martin praise the use of  
      SPARK in their C130K
      project, Eurocopter uses SCADE in safety-critical parts of the EC135;  
      so does Airbus in
      the A380, the B method has been used on rail lines in Paris, Siemens  
      uses a code-generator
      and model-comparison techniques for building the world's most complex  
      rail signalling systems,
      one of the world's major auto component suppliers uses Parnas tables  
      having suffered
      a very visible series of technical embarrassments a few years ago.
      Intel uses model checkers and theorem provers in the design of its  
      products having
      suffered a very visible embarrassment with a FP processing unit a few  
      years ago.
      Microsoft is using static analysers and annotated programming  
      languages for its new
      critical products. And so on.
      Who really thinks any of those organisations are going to go back to  
      doing things
      the way they did them before? The argument about use of formal methods  
      in industry
      has obviously been won. But you probably need to be over 50 to have  
      experienced this.
      That said, the specific argument about the use of Z and VDM and CSP  
      and so on in software
      forward development, specifically in requirements, has not been won.  
      Who here thinks
      UML 2.0 will win it?
      To my mind, the real issue is rigor and precision. Ensuring those  
      qualities takes a lot of effort.
      It took a lot of effort in the past, and it will take a lot of effort  
      in the future. There are, have been,
      and always will be people who complain about the extra effort is  
      takes. It is easy to complain,
      for safety is the absence of something. If an accident has never  
      happened to you, you may not
      want to put in that extra effort. Then it happens, as to Intel and  
      Microsoft (continually!) and the major
      auto component supplier above, and then somebody in management sees  
      the business case for
      the extra effort and, lo and behold another formal methods user.
      And you probably need to be over 45 to get impatient at seeing the  
      same old arguments
      against formal methods as a quarter century century ago being trotted  
      out yet again.
      Really, how can one ignore that the two major computer companies in  
      the world have had
      to start using them in the last decade? Microsoft employs major formal- 
      methods people such
      as Tony Hoare and Leslie Lamport well past the usual retirement ages.
      On the other hand, maybe the same old arguments are being trotted out  
      because there are eternal truths about
      the use of rigorous methods in engineering and these are some of them.  
      If this were so, then, quantifying over time,
      we could conclude:
            no formal specification languages will ever be readable, model- 
      checking will never solve anybody's
            real problems, theorem provers for refinement and code checking  
      will never be usable by engineers, static
            analysis is only for academics.
      Given that all of these already admit counter examples, I wouldn't  
      recommend believing any of it.
      Peter Bernard Ladkin, Professor for Computer Networks and Distributed  
      University of Bielefeld, 33594 Bielefeld, Germany +49 521 880 73 19
Received on Thu 06 Aug 2009 - 15:50:23 BST