This Article 
 Bibliographic References 
 Add to: 
Formal Specification and Design Time Testing
January 1990 (vol. 16 no. 1)
pp. 1-12

It is shown how design time testing can be used in conjunction with formal specification. Emphasis is placed on the benefits of using an executable specification language OBJ, of having a design controlled by requirements specification, and of adherence to the regularity and uniformity hypotheses in dynamic validation. It is shown that such an approach offers positive benefits by providing early design validation and a controlled, disciplined design process.

[1] J. A. Goguen, "Parameterized programming,"IEEE Trans. Software Eng., vol. SE-10, no. 5. pp. 528-544, 1984.
[2] C. D. Walter, R. M. Gallimore. D. Coleman, and V. Stavridou,UMIST OBJ Manual Version 1.0, Dep. Computation, UMIST, 1986.
[3] E. W. Dijkstra, "Notes on structured programming," inStructured Programming, O.-J. Dahl, E. W. Dijkstra, and C. A. R. Hoare, Eds. New York: Academic, 1972, pp. 1-81.
[4] J. B. Goodenough and S. L. Gerhart. "Towards a theory of test data selection."IEEE Trans. Software Eng., vol. SE-1, no. 2. 1975.
[5] L. Bouge et al., "Application of Prolog to Test-Sets Generation from Algebraic Specifications,"Proc Int'l Joint Conf., Theory and Practice of Software Development, Volume 2: Colloquium on Software Engineering, Springer-Verlag, New York, 1985.
[6] E. J. Weyuker and T. J. Ostrand, "Theories of program testing and the application of revealing subdomains,"IEEE Trans. Software Eng., vol. SE-6, no. 3, 1980.
[7] N. H. Gehani, "Informal and formal specifications with stepwise refinement," inInfotech State of the Art Rep. Software Eng., vol. 11, no. 3, 1981.
[8] B. W. Boehm, "Verifying and validating software requirement and design specifications."IEEE Software. Jan. 1984.
[9] M. A. Ould, Ed.,Testing in Software Development(Monographs on Informatics Series). London: Cambridge University Press. 1986.
[10] C. Jones,Software Development: A Rigorous Approach. Englewood Cliffs, NJ: Prentice-Hall International, 1980.
[11] J. K. Buckle,Software Configuration Management. New York: Macmillan, 1982.
[12] J. A. Goguen and T. Winkler, "Introducing OBJ3." Comput. Sci. Lab, SRI International, Menlo Park, CA. Tech. Rep. SRI-CSL-88-9, Aug. 1988.
[13] R. A. Kemmerer. "Testing formal specifications to detect design errors,"IEEE Trans. Software Eng., vol. SE-11, no. 1. pp. 32-42, 1985.
[14] J. V. Guttag and J. J. Homing. "The algebraic specification of abstract data types,"Acta Inform., vol. 10, pp. 27-52. 1978.
[15] J. A. Goguen, J. W. Thatcher. and E. Wagner, "An initial algebra approach to the specification correctness and implementation of abstract data types," inCurrent Trends in Programming Methodology, R. Yeh, Ed. Englewood Cliffs, NJ: Prentice-Hall, 1978, pp. 80- 149.
[16] G. Huet and D. Oppen. "Equations and rewrite rules: A survey," inFormal Language Theory: Perspectives and Open Problems. New York: Academic. 1980.
[17] Obj Ex User Reference Manual, Gerrard Software, Venture House, Macclesfield, England, 1988.

Index Terms:
formal specification; design time testing; executable specification language OBJ; regularity; uniformity; formal specification; specification languages.
C.P. Gerrard, D. Coleman, R.M. Gallimore, "Formal Specification and Design Time Testing," IEEE Transactions on Software Engineering, vol. 16, no. 1, pp. 1-12, Jan. 1990, doi:10.1109/32.44359
Usage of this product signifies your acceptance of the Terms of Use.