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

[Ken Garlington <kennieg@flash.net>]

Nick Leaton wrote:
> 
> 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.

Unfortunately, "divide and conquer" leaves open the issue of interface
validation. In addition to showing the components are valid internally,
you must also show their interactions are valid. DBC may be able to
detect (at run-time) when an invalid interaction occurs, but to
_prevent_
the invalid interaction requires much system-wide knowledge. This is
particularly true of the Ariane 5 case, where something *outside the
system* (the flight profile) was the root cause of the error. Consider
a chain of events like:

	environment generates change
	sensor senses change
	I/O device reads sensor
	software gets value from I/O device
	software does set of calculations (including generation of error term)
	error term is converted to output format [failure here]

To determine that the failure would occur, the manual reviewer must
consider the full chain to trace the relationship of the environment
definition
to the out-of-range conversion. This is easy during execution (assuming
you
have a good definition of the environment), but hard for a human. And
you have
to do this for every thread (more or less). No one will tell you in
advance
"the error term conversion is where the error is, now just figure out
why."

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

See above.

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

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

Actually, it's pretty easy, assuming you have a good definition of the
bank environment and can run adequate scenarios. It is difficult, on the
other hand, to have a system be able to internalize all of the factors
regarding its environment (no system can fully describe itself, much
less
itself and its environment!)

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

First, "running" is not early in the development process!

Second, it seems that there is a schism in the DBC community. Some feel
that
testing (execution of the code) is the important part, while others
emphasize
manual verification. It makes it very difficult to discuss the
advantages of
DBC, when the response to "it's difficult to manually verify" is "it
helps catch
errors during test" and the response to "it's difficult to use
assertions to test"
is "it helps catch errors during manual verification."

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

This is the other schism: Arguments about DBC are addressed in Eiffel
terms,
and arguments about Eiffel are addressed in DBC terms ("DBC does not
require Eiffel", for example).

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

However, most requirements are not in this form. Does this mean that
most
requirements won't be written as assertions?

Furthermore, I can get assertions of this form without DBC/Eiffel (e.g.
in
Ada, under any methodology). What's special about DBC if it causes you
to write code just to get checks you get for free in other languages?

(BTW, this is the third schism. Compare and contrast the arguments by
other
DBC/Eiffel advocates that most assertions are "high-level" abstractions,
making them easier to read. I'm pretty much convinced at this point that
DBC, like the infamous "object-oriented," can mean just about anything
to
anyone!)

> 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