Advertisement

Formal Methods and Tools: Introduction and Overview

  • R. Berghammer
  • Y. Lakhnech
  • W. Reif
Conference paper
Part of the Advances in Computing Science book series (ACS)

Abstract

For manifold reasons, the importance of software correctness is ever increasing. In particular, the application of software in highly safety critical applications demands a thorough investigation concerning its reliability and correctness. The growing awareness of the related problems has led to the establishment of the “Bundesamt für Sicherheit in der Informationstechnik” in Germany, which among others has the task to develop criteria for the evaluation of software regarding its safety and security. In the year 1990, in the IT-Evaluationshandbuch, the so-called “Green Book”, formal verification has been required as a prerequisite for the acceptance of software for safety critical applications (quality levels Q6 and Q7). Meanwhile, there exists ITSEC, the European version of the Green Book, for the evaluation of software.

Keywords

Model Check Temporal Logic Proof Obligation Proof Tree Theoretical Computer Science 
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. Alur R., Henzinger T.A. (1991): Logics and models of real-time: A survey. In: Proc. of the REX workshop “Real-time: Theory and practice”. Springer, Berlin, pp. 74–106 (Lecture notes in computer science, vol. 600)Google Scholar
  2. Boyer R.S., Moore J.S. (1979): A computational logic. Academic Press, New YorkMATHGoogle Scholar
  3. de Bruijn N.G. (1980): A survey of the project AUTOMATH. In: Essays on combina-tory logic, lambda calculus and formalism. Academic Press, London, pp. 580–606Google Scholar
  4. Burch J.R., Clarke E.M., McMillan K.L., Dill D.L., Hwang L.J. (1992): Symbolic model checking: 1020 states and byond. Information and computation 98 (2), pp. 142–170MathSciNetMATHCrossRefGoogle Scholar
  5. Clarke E., Emerson E.A. (1982): Design and synthesis of synchronization skeletonsusing branching time temporal logic. In: Proc. Workshop “Logics of programs”.Springer, Berlin, pp. 52–71 (Lecture notes in computer science, vol. 131)Google Scholar
  6. Clarke E., Grumberg O, Long D. (1993): Verification tools for finite-state concurrentsystems. In: A decade of concurrency. Springer, Berlin, pp. 124–175 (Lecture notesin computer science, vol. 803)Google Scholar
  7. Constable R.L., Johnson S.D., Eichenlaub C.D. (1982): An introduction to the PL/CV2 programming logic. Springer, Berlin (Lecture notes in computer science, vol. 135 )CrossRefGoogle Scholar
  8. Constable R.L., Knoblock T.B:, Bates J.L. (1985): Writing programs that constructGoogle Scholar
  9. proofs. Journal of Automated Reasoning 1 (3), pp. 285–326Google Scholar
  10. Constable R.L., Allen S.F., Bromley H.M., Cleaveland W.R., Cremer J.F., Harper R.W., Howe D.J., Knoblock T.B., Mendier N.P., Panagaden P., Sasaki, J.T., Smith, S.F. (1986): Implementing mathematics with the Nuprl proof development system. Prentice-Hall, LondonGoogle Scholar
  11. Dijkstra E.W. (1975): Guarded commands, nondeterminacy and formal derivation of programs. Comm. ACM 18, pp. 453–457MathSciNetMATHCrossRefGoogle Scholar
  12. Dijkstra E.W. (1976): A discipline of programming. Prentice-Hall, LondonMATHGoogle Scholar
  13. Emerson E.A. (1990): Temporal and modal logic. In: Handbook of theoretical computer science, vol. B. Elsevier, Amsterdam, pp. 995–1072Google Scholar
  14. Farmer W.M., Guttman J.D., Fäbrega F.J.T. (1996): IMPS: An updated description. In: Proc. of the 13th international conference on automated deduction. Springer, Berlin, pp. 298–302 (Lecture notes in artificial intelligence, vol. 1104 )Google Scholar
  15. Garland S.J., Guttag J.V. (1995): A Guide to LP, the Larch Prover. Systems research report 82, Digital Equipment CorporationGoogle Scholar
  16. Gordon M., Milner R., Wadsworth C. (1979): Edinburgh LCF: A mechanised logic of computation. Springer, Berlin (Lecture notes in computer science, vol. 78 )Google Scholar
  17. Gordon M. (1988): HOL: A proof generating system for higher-order logic. In: VLSIGoogle Scholar
  18. specification and synthesis. Kluwer, Amsterdam, pp. 73–128Google Scholar
  19. Gries D. (1981): The science of computer programming. Springer, BerlinCrossRefGoogle Scholar
  20. Guttag J.V. (1975): The specification and application to programming of abstract data types. Ph. D. thesis, Univ. of TorontoGoogle Scholar
  21. Goguen J., Winkler T., Meseguer J., Futatsugi K., Jouannaud J.-P. (1992): Introducing OBJ. In: Applications of algebraic specifications using OBJ. Cambridge University Press, CambridgeGoogle Scholar
  22. Hoare C.A.R. (1969): An axiomatic basis for computer programming. Comm. ACM 12, pp. 576–580, 583Google Scholar
  23. Holzmann G.J. (1990): Design and validation of protocols. Prentice-Hall, LondonGoogle Scholar
  24. Hörcher H.-M., Mikk E (1998): Test automation using Z specifications. In: Tools for system development and verification. Shaker, Aachen, pp. 107–119 (BISS mono-graphs, vol. 1)Google Scholar
  25. Huet G., Kahn G., Pauling-Mohring Ch. (1997): The coq proof assistant. Technical Report 178, INRIAGoogle Scholar
  26. Hartmanis J. (1994) About the nature of computer science. Colloquium, Fachbereich Informatik, Universität Hamburg, January 31Google Scholar
  27. Jones C.B. (1990): Systematic software development using VDM. Second edition, Prentice-Hall, LondonGoogle Scholar
  28. Kaufmann M., Moore J.S. (1997): An industrial strength theorem prover for a logic based on Commom Lisp. IEEE Transactions on Software Engineering 23 (4), pp. 203–213CrossRefGoogle Scholar
  29. Magnusson L., Nordström B. (1994): The ALF proof editor and its proof engine. In: Types for proofs and programs. Springer, Berlin, pp. 213–237 (Lecture notes in computer science, vol. 806)Google Scholar
  30. Morgan C, Vickers T. (1992): On the refinement calculus. Springer, BerlinGoogle Scholar
  31. Owre S., Rushby J., Shankar N., von Henke F. (1995): Formal verification for fault-tolerant architectures: Prolegoena to the design of PVS. IEEE Transactions on Software Engineering, 21 (2), pp. 107–125CrossRefGoogle Scholar
  32. Paulson L.C. (1987): Logic and computation. Cambridge University Press, Cambridge (Cambridge tracts in theoretical computer science, vol. 2 )MATHCrossRefGoogle Scholar
  33. Paulson L.C. (1994): Isabelle: A generic theorem prover. Springer, Berlin (Lecture notes in computer science, vol. 828 )MATHGoogle Scholar
  34. Pnueli A. (1977): The temporal logic of programs. In: Proc. of the 18th Ann. Symp. On Foundations of computer science, IEEE Computer Society, Providence, pp. 46–57Google Scholar
  35. Prior P. (1967): Past, present, and future. Oxford University Press, OxfordCrossRefGoogle Scholar
  36. Queille J.P., Sifakis J. (1982): Specification and verification of concurrent programs inCÉSAR. In: Proc. of the 5th Intern. Symp. on Programming, Springer, Berlin, pp.195–220 (Lecture notes in computer science, vol. 137)Google Scholar
  37. Reif W., Schellhoru G., Stenzel K., Balser M. (1998): Structural specifications and interactive proofs in KIV. h2: Automated deduction: A basis for applications, vol. II. Kluwer, Amsterdam, pp. 13–39Google Scholar
  38. Spivey J.M. (1992): The Z notation: a reference manual. Second edition, Prentice-Hall, LondonGoogle Scholar
  39. Thomas W. (1990): Automata on infinite objects. In: Handbook of theoretical computer science, vol. B. Elsevier, Amsterdam, pp. 134–191.Google Scholar
  40. Wirsing M. (1990): Algebraic specifications. In: Handbook of theoretical computer science, vol. B, Elsevier, Amsterdam, pp. 675–788.Google Scholar
  41. Weyhrauch R. (1981): Prolegomena to a theory of mechanized formal reasoning. In: Readings in artifical intelligence. Tioga, Palo Alto, pp. 173–191Google Scholar
  42. Woodcock J., Davis J. (1996): Using Z: specification, refinement, and proof. Prentice-Hall, LondonMATHGoogle Scholar
  43. Zilles S.N. (1974): Algebraic specification of data types. Computation structures group memo 119, Laboratory of computer science, MITGoogle Scholar

Copyright information

© Springer-Verlag Wien 1999

Authors and Affiliations

  • R. Berghammer
  • Y. Lakhnech
  • W. Reif

There are no affiliations available

Personalised recommendations