Formal Systems

  • V. S. Alagar
  • K. Periyasamy
Part of the Graduate Texts in Computer Science book series (TCS)

Abstract

Scientific experiments are of two kinds: (1) processes undertaken to discover things not yet known, (El); and, (2) processes undertaken to demonstrate things that are known, (E2). Scientific properties that have been observed will hold whenever the experiments are repeated with the same specifications, and under the same conditions. The results are independent of the scale on which the experiments are performed. Demonstrating the properties of a software system is analogous to conducting experiments of type E2. This can be done on a small scale, while establishing the properties of the software system through experiments on a reduced model of the system. However, the software development process is analogous to conducting experiments of type E l. This cannot be done on a small scale, or by employing a reduced model of the system. It is almost impossible to establish all the properties of a software system through the reduced model. It is therefore essential that software engineers get a direct exposure of the full-scale development process. On the other hand, a direct exposure of the full-scale development process may not be sufficient to reveal hidden properties of the system. A midway alternative is to adopt a certain degree of formality in software development. The motivation to espouse formal systems is driven by the quest for a foundation that is theoretically sound.

Keywords

State Machine Formal System Inference Rule Formal Language Finite State Machine 
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.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. [1]
    A.V. Aho, R. Sethi, and J.D. Ullman, Compiler Design: Principles, Techniques, and Tools, Addison-Wesley Publishing Company, Reading, MA, 1986.Google Scholar
  2. [2]
    J.W. Backus, “The FORTRAN Automatic Coding System,” Proceedings of the AFIPS Western Joint Computer Conference, 1957, pp. 188–198.Google Scholar
  3. [3]
    J. Cooke, “Formal Methods — Mathematics, Theory, Recipes or What?,” The Computer Journal, Vol. 35, No. 5, 1992, pp. 419–423.CrossRefGoogle Scholar
  4. [4]
    N. Davis, “Problem # 4: LIFT,” Fourth International Workshop on Software Specification and Design, IEEE Computer Press, April 1987.Google Scholar
  5. [5]
    E. Denert, “Specification and Design of Dialogue Systems with State Diagrams,” International Computing Symposium, D. Ribbons (Ed.), North-Holland, 1977, pp. 417–424.Google Scholar
  6. [6]
    R.J.K. Jacob, “Using Formal Specifications in the Design of a Human-Computer Interface,” Communications of the ACM, Vol. 26, No. 4, 1983, pp. 259–264.CrossRefGoogle Scholar
  7. [7]
    S.C. Johnson, “Yacc: Yet Another Compiler Compiler,” Computer Science Technical Report No. 32, Bell Labs, Murray Hills, NJ, 1975.Google Scholar
  8. [8]
    D. Harel, “Statecharts: A Visual Formalism for Complex Systems,” Science of Computer Programming, Vol. 8, 1987, pp. 231–274.MathSciNetMATHCrossRefGoogle Scholar
  9. [9]
    D. Harel, A. Pnueli, J.P. Schmidt, and R. Sherman, “On the Formal Semantics of Statecharts,” Proceedings of the Second IEEE Symposium on Logic in Computer Science, IEEE Press, NY, 1987, pp. 54–64.Google Scholar
  10. [10]
    D. Harel, H. Lachover, A. Naamad, A. Pnueli, M. Politi, R. Sherman, R. Shtull-Trauring, and M. Trakhtenbrot, “Statemate: A Working Environment for the Development of Complex Reactive Systems,” IEEE Transactions on Software Engineering, Vol. 16, No. 4, April 1990, pp. 403–414.CrossRefGoogle Scholar
  11. [11]
    S. Hekmatpour and D. Ince, Software Prototyping, Formal Methods and VDM, Addison-Wesley Publishing Company, International Computer Science Series, 1988.Google Scholar
  12. [12]
    P. Henderson, “Functional Programming, Formal Specification, and Rapid Prototyping,” IEEE Transactions on Software Engineering, Vol. SE-12, No. 2, February 1986, pp. 241–250.CrossRefGoogle Scholar
  13. [13]
    W. Hershey, “Idea Processors,” Byte, Vol. 10, No. 4, 1985.Google Scholar
  14. [14]
    J. Hoperoft and J. Ullman, Introduction to Automata Theory, Languages, and Computation, Addison-Wesley Publishing Company, Reading, MA, 1979.Google Scholar
  15. [15]
    P. Naur (ed.), “Revised Report on the Algorithmic Language Algol 60,” Communications of the ACM, Vol. 6, No. 1, 1963, pp. 1–17.Google Scholar
  16. [16]
    G. Peano, “The Principles of Arithmetic, Presented by a New Method,” in J. van Heijenoort (Ed.), From Frege to Gödel: A Sourcebook of Mathematical Logic, Harvard University Press, Cambridge, MA, 1967.Google Scholar
  17. [17]
    P. Reisner, “Formal Grammar and Human Factors Design of an Interactive Graphics System,” IEEE Transactions on Software Engineering Vol. SE-7, No. 2, March 1981, pp. 229–240.CrossRefGoogle Scholar
  18. [18]
    B. Selic, G. Gulleckson, and P.T. Ward, Real-Time Object-oriented Modeling, John Wiley & Sons, New York, NY, 1994.MATHGoogle Scholar
  19. [19]
    J.M. Wing, “A Specifier’s Introduction to Formal Methods,” IEEE Computer, Vol. 23, No. 9, September 1990, pp. 8–24.CrossRefGoogle Scholar
  20. [20]
    P. Zave, “Feature Interactions and Formal Specifications in Telecommunications,” IEEE Computer, Vol. 26, No. 8, August 1993, pp. 20–30.CrossRefGoogle Scholar

Copyright information

© Springer Science+Business Media New York 1998

Authors and Affiliations

  • V. S. Alagar
    • 1
  • K. Periyasamy
    • 2
  1. 1.Department of Computer ScienceConcordia UniversityMontrealCanada
  2. 2.Department of Computer ScienceUniversity of ManitobaWinnipegCanada

Personalised recommendations