Software Integrity Assessment

When programmers and system analysts read existing code the understanding of what objective that code is intended to achieve is partial at best. The meaning of the code is not precise. There is a way to proof-read existing code and reveal its original intent. We wrote this book to provide a means to improve the readability, correctness and understanding of the code's purpose. This is especially relevant to system design when multiple new and existing programs are brought together to...
More Description

When programmers and system analysts read existing code the understanding of what objective that code is intended to achieve is partial at best. The meaning of the code is not precise. There is a way to proof-read existing code and reveal its original intent. We wrote this book to provide a means to improve the readability, correctness and understanding of the code's purpose. This is especially relevant to system design when multiple new and existing programs are brought together to act in unison. We have accomplished this by using formal methods, and we have demonstrated the practicality of our technique by applying it within a for-profit company. In this book we introduce the basic concepts for designing, using and implementing software integrity assurance mechanisms that can provide fault-free software as well as a dependable approach to understand existing code and to support the integration of new code into existing systems. What we mean by software integrity assurance is not the same as quality assurance, which is traditionally a part of a Master of Software Engineering or Master of Computer Science degree with a Software Engineering emphasis. Software quality assurance encompasses the entire panoply of software development processes, including requirements definition, software design, coding, configuration management, testing and product integration. The use of formal methods is generally absent from the software quality assurance curriculum.Software integrity assurance, as used by us in this book, is more focused on code analysis and elimination of faults that have been introduced during the software development and maintenance phases. Our goal is to educate the reader rather than pretending to provide a magic bullet. We show the reader how to make systems cybersecure by striving to achieve fault-free systems. Our approach emphasizes the importance of using formal methods, and we explain how they form the underpinning of program and system analysis, as opposed to tracing execution paths and relying on what we call operational techniques such as test and evaluation. Software Integrity Assessment, or SIA for short, refers to our unique approach that enables you to assess the integrity of any software program or system. The book is part theory and research and another part textbook. As a first step toward fulfilling the textbook appellation we provide a summary at the end of each chapter. We intend that this summary will help the reader to more readily grasp and understand some of the more abstruse content. The idea is that the items listed in the summaries can easily be converted into exercises for the reader to solve. The intended audience for this book includes software tool designers and developers. It introduces and explains a unique way to think about software produced by others. After reading this book the reader should understand how formal methods can be used to analyze and find faults in existing software programs and systems. To realize the value of the contents to their fullest a tool needs to be developed that automates the processes described here. We have used formal methods wherever possible to facilitate the development of such a tool. Ideally the tool would translate procedural source code from a diverse set of programming languages into the formally defined declarative language we call Dijkstra Guarded Commands or DGC.