An Empirical Investigation of the Effect of Formal Specifications on Program Diversity

  • Thomas I. McVittie
  • John P. J. Kelly
  • Wayne I. Yamamoto
Part of the Dependable Computing and Fault-Tolerant Systems book series (DEPENDABLECOMP, volume 6)


Formal specification languages are increasingly being employed as an aid in the design and implementation of highly reliable systems. Recent experimental evidence indicates that the syntax and semantics associated with a formal specification language can have a large effect on the subsequent program version. This paper analyses the effect formal specification languages have on program development by examining nine diverse versions of a communication protocol created using three different formal specification languages.


Specification Language Transport Layer Program Diversity Abstract Data Type Sliding Window 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [1]
    J. Kelly and A. Avižienis, “A specification-oriented multi-version software experiment,” in Digest of 13th Annual International Symposium on Fault Tolerant Computing, pp. 120-126, June 1983.Google Scholar
  2. [2]
    P. Bishop and et al., “Project on diverse software — an experiment in software reliability,” in Proceedings IFAC Workshop Safecomp’85, 1985.Google Scholar
  3. [3]
    A. Avižienis and L. Chen, “On the implementation of n-version programming for software fault-tolerance during execution,” in Proceedings COMPSAC 77, pp. 149-155, November 1977.Google Scholar
  4. [4]
    J. Kelly and S. Murphy, “Achieving dependability throughout the development process: A distributed software experiment,” IEEE Transactions on Software Engineering, vol. SE-16, pp. 153–165, February 1990.CrossRefGoogle Scholar
  5. [5]
    J. Kelly, T. McVittie, and S. Murphy, “Techniques for building dependable distributed systems — multi-version software testing,” in Proceedings of the 20th Annual Fault Tolerant Computing Symposium, June 1990.Google Scholar
  6. [6]
    ISO, “Basic reference model for open systems interconnection,” Tech. Rep. ISO 7498, ISO, Geneva, 1984. also CCITT Recommendation X.200.Google Scholar
  7. [7]
    K. Turner, ed., Proceedings of the First International Conference on Formal Description Techniques, FORTE 88, September 1988.Google Scholar
  8. [8]
    ISO, Guidelines for the Application of Estelle, LOTOS and SDL. Stirling, January 1988.Google Scholar
  9. [9]
    ISO, “Information processing systems — OSI — LOTOS — a formal description technique for the temporal ordering of observational behavior,” Tech. Rep. ISO 8807, ISO, 1988.Google Scholar
  10. [10]
    ISO, “Estelle: a formal description technique based on an extended state transition model,” Tech. Rep. ISO 9074, ISO, 1988.Google Scholar
  11. [11]
    CCITT, “SDL, specification and description language,” (Blue Book) Z.100, International Consultative Committee for Telephony and Telegraphy, Geneva, March 1988.Google Scholar
  12. [12]
    H. Ehrig and B. Mahr, Fundamentals of Algebraic Specification, vol. 1. Berlin: Springer-Verlag, 1985.MATHGoogle Scholar
  13. [13]
    R. Milner, CCS, A Calculus of Communicating Systems, vol. 92 of LNCS. Berlin: Springer-Verlag, 1980.Google Scholar
  14. [14]
    C. Hoare, Communicating Sequential Processes. Prentice-Hall International, 1985.Google Scholar
  15. [15]
    CCITT, Recommendation T.70, Network Independent Basic Transport Service for the Telematic Services. CCITT, (red book) ed., 1984.Google Scholar

Copyright information

© Springer-Verlag/Wien 1992

Authors and Affiliations

  • Thomas I. McVittie
    • 1
  • John P. J. Kelly
    • 1
  • Wayne I. Yamamoto
    • 1
  1. 1.Department of Electrical & Computer EngineeringUniversity of California at Santa BarbaraSanta BarbaraUSA

Personalised recommendations