Re: Use of DBC as "executable SRS": scaling problems

[Ken Garlington <kennieg@flash.net>]

Nick Leaton wrote:
> 
> Ken Garlington wrote:
> 
> [snip]
> 
> > > I would believe you should be writting all. In practice they are
> > > probably written
> > > by different people, so make the assumptions transparent and executable
> > > is good
> > > practice.
> >
> > "Executable," unfortunately, doesn't help the reviewer, which was the
> > subject of my discussion. It also doesn't help if the invalid input is
> > not seen prior to operation.
> >
> > I don't know exactly what you mean by "transparent," but I assume you
> > mean "easy to read." However, that's not the issue. Consider the
> > proposed Ariane-5 Eiffel solution. The assertion #3 ( X <= Maximum )
> > is certainly easy to read. Now, prove whether or not X _will_
> > exceed Maximum for the Ariane-5. That's much more complicated,
> > since there may be a great deal of complexity hiding between the
> > system environment inputs and the value of X when it reaches this
> > assertion. Note that assertion #1 may be based on different criteria
> > than #3, so #1 may pass while #3 fail. So, adding more assertions
> > doesn't help here; in fact, it dilutes the review effort.
> 
[snip of why Eiffel assertions are easy to read - "transparent"]

How does this address the issue I raised (see quoted block above)?
Note that "transparency" is not the issue! See section 3.1.4 (in fact,
all of section 3.1) of
  http://www.flash.net/~kennieg/ariane.html

> > > > > 2) Writting assertions forces you to consider if the requirements
> > > > >    are well formed. If you can't write an assertion, has the requirement
> > > > >    been stated in an unambiguous way? Is it realisable? etc ...
> > > >
> > > > However, they cannot usually detect _missing_ requirements (Ariane 5
> > > > case).
> > >
> > > Yes. Do you have a method that does?
> >
> > Actually, there are such techniques. Failure Modes and Effects Testing
> > is very powerful for determining systems that are missing critical
> > fault-detection and fault-tolerance requirements, for example.
> 
> Nothing stops you using this.

Actually, using assertions might stop you from doing this. See section
3.1.6 of
  http://www.flash.net/~kennieg/ariane.html

> Coming back to the general point, DBC only adds to the software
> development process. It is optional. However, I do agree with Meyer in
> that you ignore it at your peril. If you are worried about timing being
> critical, which is the only valid point that I have read, I have some
> concerns.

There are more adverse consequences. See section 3.2.2 of
  http://www.flash.net/~kennieg/ariane.html

> Writing safety critical software where getting something to
> work within a set period, and you don't have a large safety margin to
> spare worrying. Similarly if you have to rely on software timings
> extensively. Getting faster chips strikes me as a better idea, or
> waiting till they become available. If you can't, you have a research
> project not a production system.

Unfortunately, flight systems such as the Ariane 5 have various
limitations
(e.g. environmental factors like available power) that may limit their
choices of hardware. (I should add this to my paper, I guess.)

I agree that it would be nice to be able to ignore such factors, but
(un)fortunately that's what makes embedded systems programming different
from other types of software development.

Note also that the issue is not that real-time systems are designed such
that they "rely on software timings extensively." The issue is testing
your system to show that it does _not_ inadvertantly rely on process
timings (e.g., race conditions). See section 3.2.2 of
  http://www.flash.net/~kennieg/ariane.html

> I would be interested in knowing more about the patterns that you use
> to handle exceptions when they happen.

That's part of the problem. Such patterns are difficult to develop.
There
are various approaches that can be used, but few have any particularly
firm proofs as to their contribution to the overall reliability of the
system. Some of this is discussed in section 3.3 of
  http://www.flash.net/~kennieg/ariane.htm

> 
> --
> 
> Nick