At 04:02 PM 12/7/2001 -0700, Vernon Schryver wrote:
I'm sorry for being so rude, but if you've been around a while, you've
seen and should have learned from the final outcomes of design processes
(including some for network protocols) that overtly involved formal
"methodologies." It's not that formal thinking is not useful and valuable,
because it is. Instead it seems that formal mechansms are always sold
as a substitute for design skill and talent, but end up consuming a lot
of both that should have been spent on designing the nominal product,
while the nominal product comes out as OSI 87 layer cake.
Now of course, I'll be told I'm all wrong, that the Space Shuttle
software is a wonderful example of how to do things right, that the
next use of a correctness prover will be for something really impressive
like a gcd algorithm that handles negative numbers, that XTP didn't
fail in the marketplace on its own defects, and similar stories.
Vern, I would say you are right but for a different reason.
Almost all formal exercises like this fail to take into account those that
live outside the rules.
In the Space Shuttle, there was little concern about onboard viruses.
I have been told that TCP was extensively modeled and reviewed. But look
at the attacks that came later.
Formal languages are nice but they are traps themselves as they limit the
allowed thinking by developers. Look at Common Criteria as yet another
example....