Software design based on operational modes

The use of software is ubiquitous despite its reputation for low reliability. This dissertation experimentally verifies this reputation and then proposes changes to the development process to prevent certain classes of failures. I begin by presenting numerous examples of software failures from modern, professionally tested, software products. The root cause of each of these failures can be traced to incorrect partitioning of internally stored data. I propose a new design technique based on a recently developed testing concept called “operational modes.” Operational modes allow correct decomposition (abstraction) of software states defined by storage constraints and describe the cause of a large class of software failures. Operational mode design is influenced by four constraining software features: input, output, computation, and data storage. From this understanding, four classifications of failure are derived from this improved definition of operational modes: (1) improperly constrained input, (2) improperly constrained output, (3) improperly constrained computation, and (4) improperly constrained internal data. Illustrative examples of these failure classes are presented from a number of published programs. I propose changes to the software design process to eliminate these four identified categories of defects by proper identification and implementation of system constraints, i.e., operational modes that correctly partition program data. This new theory provides developers a methodical mechanism to prevent a large class of software faults and provides software testers a roadmap to the broad class of software behaviors that must be tested. I demonstrate the application of this design process modification with a small example that, though proven to be correct in the literature, fails due to lack of proper constraint checking. The resulting example program no longer contains these defects as a direct result of the improvements to the design process. The process is further verified by redesigning an example program from a modern software development text. Not only does the technique correct a defect in that example, but results in a function that is now clearly specified and eliminates the need to rely on “clever” design to achieve the desired results.