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

[Nick Leaton <nickle@calfp.co.uk>]

card@syr.lmco.com wrote:
> 
> 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.

Divide and conquer still applies. One would hope that the component
pieces of your system will still small. Using assertions at this level
is an advantage. 

 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.

Assertions help with verification and validation. 

1) Violations get caught early in the design process. 
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 ...
3) There are requirements that cannot be coded as assertions. For
   example a bank may have a requirement that the software should
   try and prevent the bank becoming bankrupt. Perfectly normal 
   requirement. The software can help perform this task. However,
   stated as such, you cannot code it. You have a problem testing it.
4) Is having assertions on utility classes and verifying them, writing
   requirements for them a problem?


>     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.

Again, having the assertions in place, and having the verification and
validation performed automatically as you run makes it more likely that
you find the errors early rather than latter.

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

But the impact of it is, as you are more likely to catch it earlier.
Remember, you don't have to write the assertions. ie. Eiffel is giving
you an extra tool.

> (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.

Assertions are inherited. It is common for base classes to have lots of
assertions, deferred features (virtual in C++ parlance). Inherit classes
don't have many as they have inherited the assertions.

>     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.

Most assertions are of this form. Checks that a reference is not void.
As a result they are cheap to evaluate. In other systems you add
such checks into the implementation, so you have to do them anyway.

> 
> 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.

Again not true in practice. You are building large systems out of small
systems. Why shouldn't the requirements of small systems utilise DBC.
You cannot lose anything, only gain.

Some requirements cannot be stated in any language easily as you have
pointed out. Some assertions cannot be easily, or efficiently code in
Eiffel (or other languages)

Before I started using Eiffel, I had similar doubts as you had about
assertions, including the fact that I didn't think programmers would use
them, being lazy, under preasure ... However you do write them, and
think hard about them. This is for the reason I've stated earlier, you
catch mistakes earlier in the development process, and writing them
makes your design clearer.

-- 

Nick