Firmware testing and test data selection

ABSTRACT

Loosely stated, program verification is the task of systematically demonstrating that a program achieves its intended purpose, i.e., the task of proving the absence of errors from a program. This task may be considered as a backward mapping from a given program to a statement of the requirements for that program. There exist two fundamental approaches to establishing such mappings. A program may be exercised for a specific set of input values; the successful completion of program execution constitutes a necessary condition for the correctness of that program. A more rigorous approach is to provide an argument that a program satisfies its requirements for all legitimate input values, thus constituting a necessary and sufficient condition for the correctness of that program. In this paper, we are concerned with the first of these two fundamental approaches.

REFERENCES

• 1: Joseph E. Stoy, Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory, MIT Press, Cambridge, MA, 1977
• 2: Floyd, R. W., "Assigning Meaning to Programs", Proc. of Symposia in Applied Mathematics, American Mathematical Society, Vol. 19, 1967, pp. 19--32.
• 3: C. A. R. Hoare, An axiomatic basis for computer programming, Communications of the ACM, v.12 n.10, p.576-580, Oct. 1969 [doi>10.1145/363235.363259]
• 4: Helmut K. Berg, Correctness of Fireware - An Overview, Firmware Engineering, Seminar veranstaltet von der gemeinsamen Fachgruppe "Mikroprogrammierung" des GI Fachausschusses 3/4 und des NTG-Fachausschusses 6 vom, p.173-224, March 12-14, 1980
• 5: Dijkstra, E. W., "Notes on Structured Programming," Technical University Eindhoven, Tech. Report EWD 149, April 1970.
• 6: Goodenough, J. B.; Gerhart, S. L., "Toward a Theory of Test Data Selection", IEEE Trans on Software Engineering, Vol. 1, No. 2, 1975, pp. 20--37.
• 7: R. E. Fairley, Tutorial: Static Analysis and Dynamic Testing of Computer Software, Computer, v.11 n.4, p.14-23, April 1978 [doi>10.1109/C-M.1978.218132]
• 8: Berg, H. K.; Boebert, W. E.; Franta, W. R.; Moher, T. G., "A Survey of Formal Methods of Program Verification and Specification", Digital Systems Program, University of Minnesota, DSP-79-02.
• 9: P. C. Poole, Debugging and Testing, Software Engineering, An Advanced Course, Reprint of the First Edition [February 21 - March 3, 1972], p.278-318, January 1975
• 10: Stucki, L. G.; Svegel, N. P., "Software Automated Verification System Study", McDonnell Douglas Astronautics Corp., Rep. AD-784086, 1974.
• 11: Berg, H. K., "A Model of Timing Characteristics in Computer Control", EUROMICRO Journal, Vol. 5, No. 4, 1979, pp. 2067--218.
• 12: Davidson, S.; Shriver, B. D., "Firmware Engineering: An Extensive Up-date", Firmware, Microprogramming, and Restructurable Hardware, North-Holland Publ. Co., 1980, pp. 1--40.
• 13: Lewis, T. G.; Malik, K.; Ma, P.-Y., "Firmware Engineering Using a High-Level Microprogramming System to Implement Virtual Instruction Set Processors", Firmware, Microprogramming and Restructurable Hardware, North-Holland Publ. Co., 1980, pp. 65--87.
• 14: Dasgupta, S., "Some Implications of Programming Methodology for Microprogramming Language Design", Firmware, Microprogramming, and Restructurable Hardware, North-Holland Publ. Co., 1980, pp. 243--252.
• 15: Berg, H. K.; Franta, W. R., "Firmware Engineering: Critical Remarks and a Proposed Strategy", Firmware, Microprogramming and Restructurable Hardware, North-Holland Publ. Co., 1980, pp. 41--64.
• 16: Richter, L., "High-Level Language Extensions for Micro-Code Generation and Verification", Firmware, Microprogramming and Restructurable Hardware, North-Holland Publ. Co., 1980, pp. 233--242.
• 17: Crocker, S. D.; Marcus, L.; van-Mierop, D., "The ISI Microcode Verification System", Firmware, Microprogramming and Restructurable Hardware, North-Holland Publ. Co., 1980, pp. 89--103.
• 18: D. A. Patterson, Strum: Structured Microprogram Development System for Correct Firmware, IEEE Transactions on Computers, v.25 n.10, p.974-985, October 1976 [doi>10.1109/TC.1976.1674538]
• 19: Carter, W. C.; Joyner, W. H.; Brand, D., "Microprogram Verification Considered Necessary," Proc NCC 1978, AFIPS Conference Proceedings, Vol. 47, 1978, pp. 657--664.
• 20: Kamran Malik , Ted Lewis, Design objectives for high level microprogramming languages, Proceedings of the 11th annual workshop on Microprogramming, p.154-160, November 19-22, 1978, Pacific Grove, California, United States
• 21: Davidson, S., Shriver, B. D., "MARBLE: A High Level Machine Independent Language for Microprogramming", Firmware, Microprogramming, and Restructurable Hardware, North-Holland Publ. Co., 1980, pp. 253--266.