Reading suggestions for discussion group on bugs, module CO721A, 2010/2011
The practice of software testing was once famously dismissed by Edsger Dijkstra (a key figure in computer science), who stated that "testing shows the presence of bugs, but cannot show their absence". Was he right?
Below are some of references I suggested during our first meeting.
Note that it is not necessary that all of you read all of these
things. And certainly anyone willing to find, read and discuss with
other members some alternative references is more than welcome to.
This is just to suggest some of possible issues you can discuss and to
provide you with pointers to the literature.
You can find some information about contemporary, state of art
solutions in part III below (this is just to ensure you won't get discouraged
halfway in the middle of this long list)
- Motivation
- A long list of disastrous programming errors:
http://www.cs.tau.ac.il/~nachumd/horror.html
- a few articles on most famous software bugs:
PC World (recommended!)
http://www.pcworld.com/article/205318/11_infamous_software_bugs.html
Computerworld blog: Can malware kill?
http://blogs.computerworld.com/16801/murder_by_malware_can_computer_viruses_kill
[but do malware issues deserve the name of software bugs? ]
Wired's History worst software bugs:
http://www.wired.com/software/coolapps/news/2005/11/69355
[would you really say all issues described in this article deserve the name of software bugs? compare it with the PC World article above]
You can easily find more: google for software bugs
- an example that a potential bug can be hidden even in most innocent
part of programs, including standard libraries and procedures "proved"
to be correct
Google blog: nearly all binary searches are broken
http://googleresearch.blogspot.com/2006/06/extra-extra-read-all-about-it-nearly.html
[you might find heated discussion below interesting as well]
Another paper on the same subject:
http://www.di.unipi.it/~ruggieri/Papers/semisum.pdf.
And a paper taking this observation as a starting point:
http://portal.acm.org/citation.cfm?id=1190234
[this already belongs to part III below]
- Background
- The preface and first chapter of Notes on Programming by Alexander
Stepanov:
http://www.stepanovpapers.com/notes.pdf
Take a look, in particular, at his seven principles on page 3. What do
you think about them? Do you understand them all? Do you sometimes come
to similar conclusions in your programming practice? Or perhaps you
disagree with him? Ditto for his discussion of top-down design in the
same chapter.
- some lectures of Turing award winners (see
http://en.wikipedia.org/wiki/Turing_Award for more on Turing award
itself)
- The Humble Programmer - Turing award lecture of E. W. Dijkstra in
1972, perhaps the most famous source for the quote we are discussing about:
http://www.cs.utexas.edu/~EWD/ewd03xx/EWD340.PDF
Except for the crucial question was he right? there are a few others worth asking. For example: which points in this lecture remain valid until today?
Discuss his three conditions and six arguments. Why was he so skeptical of testing and what does he propose instead? What do you think about his view on the influence of the
choice of programming language, notation and tools on programmer's
thinking?
Contrast the outcome of your discussion with some contemporary literature on the subject, in particular papers listed in part III below. In the light of these developments, are some points in this lecture worth rethinking? Can we do today at least some of the things Dijkstra considered desirable but did not have sufficient tools at hand?
And, moreover, is he concerned only with verification or does he have some larger issues in mind - for example, the way you write your code?
Other Turing award lectures on similar subjects:
-
Computer programming as an art - Donald Knuth in 1974
http://portal.acm.org/citation.cfm?id=361612
What is root of all evil (or at least most of it) in programming
according to Knuth? Do you agree with this point? And with his views on
the role of aesthetics in computer programming?
- Emperor's old clothes - Tony Hoare in 1980
http://www.cs.ucsb.edu/~ravenben/papers/coreos/Hoa81.pdf
Some points to discuss: find in the lecture the famous quote on two
ways of constructing a software design. Do you understand these two
ways? Do some programming languages and tools lend themselves to the
method of software design recommended by Hoare more easily than others
(compare this with discussion of Dijkstra above)? What does he say in
this respect of design of particular programming languages, such as
Algol 60 and its subsequent versions, PL/1 and Ada? What are the
reasons Hoare gives for the failure of the first major project he was
involved with? Are there any lessons you can draw for this story for
your own future commercial projects? What does Tony Hoare say about
dangers of unreliable programs and programming?
- For a slightly different point of view and a good historical
overview see an article by S. Shapiro
Splitting the difference: the
historical necessity of synthesis in software engineering.
http://dx.doi.org/10.1109/85.560729
What does he say about ideas and hopes such as those expressed in
lectures of Hoare and Dijkstra above? Do you agree with his criticism
of these?
Contrast all this with information about contemporary, state of art
solutions as described in papers suggested in part III below.
-
- See the wikipedia entry on Verification and Validation. What these
two notions correspond to in software engineering?
- But also have a careful look at the wikipedia software verfication article.
First, it clearly discusses testing as belonging into dynamic software verification stage (rather than validation). On the other hand, the only method mentioned explicitly in
the wikipedia article on software validation
is... dynamic testing. This illustrates the dangers of assuming that wikipedia is uniformly consistent and reliable reference. Much more on validation can be found in the general
article on verification and validation (i.e., not focusing specifically on software)
- Yet another issue with consistency of all these definitions and classifications: the wikipedia article on static testing says
From the black box testing point of view, static testing involves reviewing requirements and specifications. This is done with an eye toward completeness or appropriateness for the task at hand.
This is the verification portion of Verification and Validation.
Now, if you define verification in the standard way as checking whether the code meets specification, you'd hence assume that
- specification is finished before verification commences and
- verification deals only with correctness of code, not of specification.
But then it would not make sense to say (as the wikipedia article does) that what is supposed to be a part of verification process can involve reviewing specification or requirements -
do you see what I have in mind?
- Note also that wikipedia has both articles on formal methods and formal verification, which clearly implies that these are separate notions.
Formal methods can be used in at least two ways (see http://en.wikipedia.org/wiki/Formal_methods for details):
- Producing a specification. If you don't use formal tools later on and simply develop informally program on the basis of formal specification,
this is what the wikipedia article calls "formal methods lite". In this case, we cannot speak of "formal verification" at all,
despite formal methods being used at some early stage of development (but this already can decrease the number of bugs and the wikipedia article suggests that at times
it might the most cost-effective solution).
- Formal methods can be used in actual verification. Note that peforming stage 1 above (i.e., producing a formal specification) is a necessary prerequisite for this step.
There is a separate wikipedia article on formal verification.
As you see, model checking (which again breaks down into many possible specific techniques - check which ones!) is just one of two possible main approaches to formal verification.
Another approach focuses on logical inference and can either
- involve only proofs conducted by humans (which does not mean being informal!) or
- be partially automated or
- be fully automated, with a multitude of possible tools (check which ones!).
- Some examples of contemporary, state of art solutions, tools,
methodologies and research projects.
-
G. Klein et al. seL4: Formal Verification of OS Kernel
http://www.sigops.org/sosp/sosp09/papers/klein-sosp09.pdf
How do authors blend traditional operating systems and formal methods
techinques? What are simplifying assumptions they make and what they do
to make their project and methodology as close to real world as
possible? What are the formal tools they are using? How does their
design process look like? What are the refinement layers in their
verification process? What lessons can be drawn from this work
concerning design, specification, implementation, verification and
testing? Do some of authors' points mesh in views expressed by Dijkstra?
An article disputing the cost of Klein et al. work can be found here:
http://www.eetimes.com/discussion/break-points/4027546/Code-Getting-it-Right
You can contrast his claims about person years with Section 5.2 of Klein et al. article. Please do note that:
- even in comments section below the article people dispute author's calculations
- some references on the reading list above mention (see, e.g., p. 26 of Shapiro article)
a famous 1975 book The Mythical Man-Month questioning the whole point of such units as man-months or person-years (although in a slightly different context)
- the SEL4 microkernel is not the only OS which claims to have been formally proved correct. Another one can be found under these links:
http://en.wikipedia.org/wiki/Integrity_(operating_system)
http://www.darkreading.com/security/app-security/showArticle.jhtml?articleID=212100421
http://www.ghs.com/products/rtos/integrity.html
http://www.ghs.com/products/safety_critical/integrity-do-178b.html
-
G. Klein Operating system verification--an overview
http://www.springerlink.com/content/4114815580rq8146/
The first two sections bring some information about software
verification in general. What are criteria evaluation levels? What are
software verification artefacts? What is the basic promise of software
verification? Section 4 brings some information about state of art;
there is some overlap with the paper quoted above. Again, contrast this
article with Dijkstra lecture. According to the author, has anything
changed in recent years and made a partial realization of Dijkstra's
vision more likely?
-
B. Cook et al. Termination proofs for system code
http://research.microsoft.com/en-us/um/cambridge/projects/terminator/binreach.pdf
What sort of tool the authors are describing? How does it relate to the
first paper suggested above in this part? Why there was a need for such
a tool? What exactly does it do and why does it work?
Here you can find more information:
http://research.microsoft.com/en-us/um/cambridge/projects/terminator/
-
Yet another paper Better avionics software reliability
http://www-wjp.cs.uni-sb.de/publikationen/Ba09EW.pdf
-
and many else... try to find something yourself
see also wikipedia entries on: Isabelle, software engineering [lots of
references], software testing
- In autumn of 2010, prof. Nancy Leveson from MIT visited DMU - the other university in Leicester.
Her webpage and her papers do provide a lot of information on the present state of art in areas as diverse
as aerospace, nuclear power, energy and petroleum, transportation, aircraft, and medical systems
-
For a very unorthodox view of software engineering, you can also have a
look at W. Daniel Hillis essay Close to singularity
http://www.edge.org/documents/ThirdCulture/zh-Ch.23.html
What does he say about engineering process? Would you trust software
produced according to his vision? Compare this essay with some recent
papers in software verification listed above.
A certain irony lies in the fact that his company Thinking Machines
mentioned in this essay went bankrupt more or less at the same time
essay was written. Here you can find more information:
http://www.inc.com/magazine/19950915/2622.html
- Additional reading:
- Software development methodologies:
http://en.wikipedia.org/wiki/Software_development_methodology
http://www.techbookreport.com/SoftwareIndex.html
- Some time ago, a colleague suggested to me the book
Scrappy Project Management
http://www.amazon.com/Scrappy-Project-Management-Predictable-Avoidable/dp/1600050514
Haven't read most of it it yet and it's not even about programming.
However, what strikes one almost immediately is the similarity between
project failures the author describes and the origin of disastrous bugs
as described in articles form Part I or the reasons for programming
failures discussed by Tony Hoare. If anyone wants to have a go at this
book and tell us whether it might contain interesting lessons for
software developers , this can lead to a pretty interesting discussion.
Tadeusz Litak
last modification 16 March 2011