Formal Specification Techniques for Interactive Systems

  • Marie-Claude Gaudel
Conference paper
Part of the Eurographics book series (EUROGRAPH)


This paper summarises a survey presentation on formal specification techniques and formal development methods. Currently, there is a significant amount of interest in the application of these methods to the specification, design, validation and verification of interactive systems (see for instance [9, 14] and several papers in these proceedings). This leads to the following questions: are general purpose techniques applicable? Is it better to design a specific formal approach for this kind of system?

After a brief survey of the main mature techniques, some examples of techniques specific to some application domains are discussed.


Formal Method Interactive System Specification Language Deduction System Communicate Sequential Process 
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.
    Aho A., Sethi R., Ullmann J., Compilers, Addison-Wesley, 1986.Google Scholar
  2. 2.
    Arnold A., Gaudel M-C., Marre B., An Experiment on the Validation of a Specification by Heterogeneous Formal Means: the Transit Node, March 1995.Google Scholar
  3. 3.
    Palanque Ph., Bastide R., Spécifications Formelles pour l’ingiénirie des interfaces homme-machine, Technique et Science Informatique, vol. 14, n° 4, pp. 473–500, 1995.Google Scholar
  4. 4.
    Bidoit M., Kreowski H.-J., Lescanne P., Orejas F., Sannella D. (editors), Algebraic System Specification and Development: a survey and annotated bibliography, LNCS n° 501, Springer Verlag, 1991.MATHGoogle Scholar
  5. 5.
    Bidoit M., Gaudel M.-C., Mauboussin A., How to make algebraic specifications more understandable ? An experiment with the PLUSS specification language, Science of Computer Programming, Vol. 12, n°1, June 1989, pp. 1–38.CrossRefGoogle Scholar
  6. 6.
    Chretienne P., Timed Petri Nets, Journal of Systems and Software, vol. 6, 1986.Google Scholar
  7. 7.
    Craigen D., Kromodimoeljo S., Meisels I., Pase B and Saaltink M., EVES: an overview, LNCS n° 551, Springer Verlag, 1991, pp. 389–405.Google Scholar
  8. 8.
    Craigen D., Gerhart S., Ralston T., On the use of formal methods in industry -an authoritative assessment of the efficacy, utility, and applicability of formal methods to systems design and engineering by the analysis of real industrial cases, Report to the US National Institute of Standards and Technology, March 1993.Google Scholar
  9. 9.
    Dix A. J., Formal Methods for Interactive Systems, Computers and People, Academic Press, London, 1991.Google Scholar
  10. 10.
    Emerson E.A., Temporal and Modal Logic, in Handbook of Theoretical Computer Science, vol. 8, Van Leeuwen J. editor, Elsevier, 1990.Google Scholar
  11. 11.
    Garlan D. and Delisle, N. “Formal Specifications as Reusable Framework”, VDM’90, LNCS n° 428, Springer Verlag, 1990, pp. 150–163.Google Scholar
  12. 12.
    Gaudel M-C., Algebraic Specifications, Chapter 22 of Software Engineer’s Reference Book, John McDermid ed., Butterworths, 1991.Google Scholar
  13. 13.
    Harel D., Statecharts: a visual formalism for complex systems, Science of Computer Programming, Vol.8, n°3, June1987, pp. 231–274.CrossRefMathSciNetGoogle Scholar
  14. 14.
    Harrison M., Thimbleby H., (editors), Formal Methods in Human-Computer Interaction, Cambridge University Press, 1990.MATHGoogle Scholar
  15. 15.
    Hoare C.A.R., Communicating Sequential Processes, Prentice Hall International, 1985.Google Scholar
  16. 16.
    ISO, LOTOS, IS-8807, 1989.Google Scholar
  17. 17.
    Jones, C.B. Systematic Software Development using VDM, 2nd edition, Prentice Hall, 1990.Google Scholar
  18. 18.
    Lincoln P. and Rushby J., A Formally Verified Algorithm for Interactive Consistency under a Hybrid Fault Model, IEEE 23th International Symposium on Fault-Tolerant Computing (FTCS), 1993, pp. 402–411.Google Scholar
  19. 19.
    Maibaum T., Taking more of the Soft out of Software Engineering, IEEE International Workshop on Software Specification and Design (IWSSD 93], 1993, pp. 2–7.CrossRefGoogle Scholar
  20. 20.
    Milner R., A Calculus of Communicating Systems, LNCS n° 92, Springer Verlag, 1980.Google Scholar
  21. 21.
    Neilsen M., Havelund K., Wagner K. and George C., The RAISE Language, Method and Tools, Formal Aspects of Computing, vol 1, n° 1, 1989, pp. 85114.Google Scholar
  22. 22.
    Rushby J., Formal Methods and the Certification of Critical Systems, SRI-CSL-93–07 report, Nov. 1993, 308 pages.Google Scholar
  23. 23.
    Spivey J.M., The Z notation: a reference manual, Prentice Hall International, 2nd edition, 1992.Google Scholar

Copyright information

© Springer-Verlag/Wien 1995

Authors and Affiliations

  • Marie-Claude Gaudel
    • 1
  1. 1.LRI, URA 410 du CNRSUniversité de Paris-SudOrsayFrance

Personalised recommendations