Yechiel Kimchi (CS,Technnion)
Wednesday, 5.4.2017, 12:30
The theory of software creation (aka programming) relies on several theoretical domains: Computability, complexity, algorithms, graph theory, and alike. Alas, the above are related to only a narrow facet of the quality of the software - functional correctness and performance.
When software is created automatically, correctness and performance may be enough. Until then, two decades or more into the future, quality software is also measured by usability, testability, and modifiability, which none of them is affected by the above theories. Moreover, the latter two of them undoubtedly affect functional correctness.
In reality, there is a theory that supports software quality, and it addresses human cognition limitations as well as computational limitations(*). Unfortunately, I am able to prove that the theory that supports software quality is mostly ignored in the industry, and the resulting modus vivendi is that buggy general purpose software is acceptable. Given that state, one should worry whether safety-critical systems are better, and if they are, in what sense they are better.
My presentation concentrates on the stages at which the software is created: design, coding, and testing. The purpose of this presentation is to prove that even safety-critical software systems are developed while ignoring the theory related to software quality (I will show it for MISRA-C, the motor industry standard, and for JSF-C++, the F-35 software standard). The fact that software based on such standards has less bugs than general purpose software can be explained by the humongous testing it goes under, resulting with losing both time and money.
The presentation deals with the software quality theory in a language-independent style, while a few examples will be given using C and C++. Time permitting, I will argue that the remedy employed by the industry concentrates on the process of the software development. While I do not deny the importance of a good process in order to carry out a complicated task, be it as it may, it neither replaces the theory, nor can it be successful when a team of software engineers is managed as a team of football players, while managing them as a team of chess players seems much more adequate.
(*) No formal-verification tool is able to test a single property of a full system - even one that is not limited by Godel's incompleteness theorem - because the actual state-space is just too big.