Verification and Validation of Real-Time Software

ISBN-13: 9783642702266 / Angielski / Miękka / 2011 / 246 str.

William J. Quirk

Opis

W.J.Quirk 1.1 Real-time software and the real world Real-time software and the real world are inseparably related. Real time cannot be turned back and the real world will not always forget its history. The consequences of previous influences may last for a long time and the undesired effects may range from being inconvenient to disastrous in both economic and human terms. As a result, there is much pressure to develop and apply techniques to improve the reliability of real-time software so that the frequency and consequences of failure are reduced to a level that is as low as reasonably achievable. This report is about such techniques. After a detailed description of the software life cycle, a chapter is devoted to each of the four principle categories of technique available at present. These cover all stages of the software development process and each chapter identifies relevant techniques, the stages to which they are applicable and their effectiveness in improving real-time software reliability. 1.2 The characteristics of real-time software As well as the enhanced reliability requirement discussed above, real-time software has a number of other distinguishing characteristics. First, the sequencing and timing of inputs are determined by the real world and not by the programmer. Thus the program needs to be prepared for the unexpected and the demands made on the system may be conflicting. Second, the demands on the system may occur in parallel rather than in sequence.

Spis treści

1 Introduction.- 1.1 Real-time software and the real world.- 1.2 The characteristics of real-time software.- 1.3 Problems of real-time software.- 1.4 Experience to date.- 1.5 Design for reliability.- 1.6 Outline of this report.- 2 Software Reliability and the Software Life Cycle.- 2.1 Real-time system development environments.- 2.1.1 Real-time system life cycles.- 2.1.2 System life cycle and system quality.- 2.1.3 Licensing and the system life cycle.- 2.2 Traditional system development phases.- 2.2.1 Requirements specification.- 2.2.2 Software design.- 2.2.3 Coding.- 2.2.4 Integration.- 2.2.5 Maintenance.- 2.3 Verification and validation.- 2.3.1 Requirements specification verification.- 2.3.2 Design verification.- 2.3.3 Code verification.- 2.3.4 System validation.- 2.3.5 Verification and validation documentation.- 2.4 Unified system development environments.- 2.4.1 The importance of the data base.- 2.4.2 A formal basis for production environments.- 2.4.3 Abstraction as the unifying basis of system production.- 2.4.4 Recommendations for the development environment.- 2.5 Current real-time application examples.- 2.5.1 Use of formal requirements specifications.- 2.5.2 Use of program design languages and design checkers.- 2.5.3 Use of verification techniques and automated tools.- 2.6 Conclusions.- 3 Structural Analysis and Proof.- 3.1 Structural analysis.- 3.1.1 Simple techniques.- 3.1.2 SPECK.- 3.1.3 Petri nets.- 3.1.4 Other net models.- 3.2 Proving techniques.- 3.2.1 Hoare’s approach to proving program correctness.- 3.2.2 Proof of termination.- 3.2.3 Treatment of arrays.- 3.2.4 Theorem proving in general.- 3.2.5 Proving timing properties.- 3.2.6 Proofs of parallel programs.- 3.2.7 Practical application of the techniques.- 3.3 Fault tree analysis.- 3.3.1 Fault tree analysis for software.- 3.3.2 Features of the approach.- 3.4 Review techniques.- 3.4.1 Inspection method.- 3.4.2 Walk through.- 3.4.3 Comparison.- 3.4.4 Tools.- 3.4.5 Effort and effectiveness.- 3.5 Conclusions.- 4 Systematic Testing.- 4.1 Practical aspects of testing real time programs.- 4.2 Glass box testing.- 4.2.1 Path testing.- 4.2.2 Path domain testing.- 4.2.3 Path predicates and specifications.- 4.2.4 Mutation analysis.- 4.2.5 Symbolic execution.- 4.2.6 Problems.- 4.3 Black box testing.- 4.3.1 Positive testing.- 4.3.2 Negative testing.- 4.4 Hierarchic testing.- 4.4.1 Top-down testing.- 4.4.2 Bottom-up testing.- 4.4.3 Comparison.- 4.4.4 Regression testing.- 4.5 Test data.- 4.5.1 Test input data generation.- 4.5.2 Test output data calculation and comparison.- 4.6 Test evaluation.- 4.6.1 Metrics.- 4.6.2 Effects of probes.- 4.7 Use of tools.- 4.8 Conclusion.- 5 Statistical Testing of Real Time Software.- 5.1 When to apply statistical testing techniques.- 5.2 The statistical test aim.- 5.2.1 General.- 5.2.2 Risk considerations.- 5.3 Simple cases.- 5.3.1 The independency question.- 5.3.2 Time windows.- 5.3.3 Sequences of tasks.- 5.3.4 Interrupts, priorities, reentrancy.- 5.3.5 Profiles of analog input signals.- 5.3.6 Testing of time constraints.- 5.3.7 Probability of exhaustive testing.- 5.4 Reliability growth models.- 5.5 Testing large systems.- 5.5.1 General.- 5.5.2 Testing for freedom from errors.- 5.5.3 Testing for failure during operation.- 5.5.4 Testing with respect to risk.- 5.5.5 Criticism.- 5.6 Testing of diverse systems.- 5.6.1 Diversity versus singularity.- 5.6.2 Test effort in diverse systems.- 5.6.3 Criticism.- 5.7 Problems with large tests.- 5.8 Conclusions.- 6 Simulation and System Validation.- 6.1 Simulation of plant as a testing aid.- 6.1.1 Simulation and diversity.- 6.1.2 Effectiveness of simulation as a validation technique.- 6.1.3 Continuous system simulation construction.- 6.1.4 Discrete system simulation construction.- 6.1.5 Example of the use of simulation.- 6.2 Simulation of the system itself.- 6.2.1 System functionality and interfaces.- 6.2.2 System performance simulation.- 6.2.3 System design simulation.- 6.2.4 System error simulation.- 6.2.5 Simulation and operator interfaces.- 6.2.6 Simulation throughout system development.- 6.3 Conclusion.- 7 Conclusion.- 7.1 Review of the problem.- 7.2 The methods reported.- 7.3 Hints for practical use.- 7.3.1 V&V during system development stage.- 7.3.2 V&V activities after the coding stage.- 7.3.3 V&V of systems with operating experience available.- 7.4 Final remark.- References.- Appendix I Proof of formula 5.7.- Appendix II Derivation of formulae 5.8 through 5.11.- Appendix III Proofs of formulae 5.14 through 5.17.