Use of DBC as "executable SRS": scaling problems

[card@syr.lmco.com]

During the Ariane thread, some stated or implied that Eiffel's inclusion
of
preconditions and postconditions in method signatures and invariants in
class
specifications would have made the software more verifiable since the
software requirements would have effectively been coded right into the
class
definitions.

I do not think that using DBC as an "executable SRS" (SRS == Software
Requirements Specification) would have necessarily saved the Ariane V (I
am
not going to revisit the issues of testing & verification, etc). The
reasons I
think this way are not due to any inherent flaws in the DBC concept
itself,
but rather are due to problems of scale:

(1) In a large and complex system, the number of preconditions and post-
    conditions in a complex class hierarchy could get extremely large. I
was
    a member of a team which built a real-time database manager for the
Seawolf
    submarine. This software component had over 300 requirements, and we
had to
    verify almost all of them by test (there were a *very small* number
that
    were verified by inspection). These tests included timing tests that
were
    conducted on the actual hardware that was delivered to the Seawolf.

    In a large system like this, the verification and validation (V & V)
    process is difficult. It is hard to keep track of 300+ requirements,
    especially since those requirements frequently change during the
    development of the system! (It took a team of 3+ people about 2.5
years
    to build and verify the Seawolf's database manager). If the
requirements
    are expressed in code that is part of your method signatures, the task
    will not (IMHO) get any easier. In fact, it would likely get worse
since
    there would be additional assertions on low-level "utility" classes
    that are not part of the system's requirements.  These would also have
to
    be verified against another set of requirements.

    In the end, you would have a *very large* number of assertions to keep
    track of and update as the system's requirements changed. Making sure
    that the changes in your requirements baseline get into the assertions
    correctly would be just as difficult as making sure they get into the
    method bodies correctly, in my view.

    The chance for an error under these conditions is not lessened by DBC.

(2) If DBC were used as an "executable SRS", the number of assertions in
the
    system could very easily grow so large as to cause deadlines to be
missed.
    I suppose that most Eiffel programmers would write preconditions in
terms
    of public attributes (i.e. require (My_Object.Attr_1 = whatever)), but
    even simple comparisons like this could really add up if there are
enough
    of them. This point is only of concern for developers of large
real-time
    systems.

I am not saying here that I think DBC is inappropriate for large real-time
systems. On the contrary, I think that selective application of it might
be
of real benefit in some systems. What I am criticizing is the notion that
DBC
can be used to basically code the system requirements right into the
mission
software ("provably correct S/W courtesy of DBC"). This might be true for
some
very small systems, but on the large systems I have worked on I think an
approach like this would have failed miserably due to the two scaling
problems
mentioned above. I do not know how large the software system on Ariane V
was,
but I suspect it was too large for an approach like this.

-------------------==== Posted via Deja News ====-----------------------
      http://www.dejanews.com/     Search, Read, Post to Usenet