Advertisement

Introduction to Subject Area “Verification”

  • Frank Ortmeier
  • Wolfgang Reif
  • Gerhard Schellhorn
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3147)

Abstract

Over the last two decades the use of software in technical applications has dramatically increased. Almost all real-world systems are now embedded systems consisting of hardware and software components. Just think of modern automobiles; every new car comes equipped with computers that have many tasks in almost all parts of the car: fuel injection rates of the engine, airbags, anti-blocking systems (ABS) for brakes or the anti-theft device are some examples.

Keywords

Safety Property Object Management Group Hybrid Automaton Fault Tree Analysis Fault Tree Analysis 
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.
    CoFI (The Common Framework Initiative): Casl Reference Manual. LNCS 2960 (IFIP Series). Springer (2004) Google Scholar
  2. 2.
    Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Englewood Cliffs (1985)zbMATHGoogle Scholar
  3. 3.
    Jones, C.B.: Systematic Software Development using VDM, 2nd edn. Prentice-Hall, Englewood Cliffs (1990)zbMATHGoogle Scholar
  4. 4.
    Spivey, J.M.: The Z Notation: A Reference Manual, 2nd edn. International Series in Computer Science (1992)Google Scholar
  5. 5.
    Abrial, J.R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press, Cambridge (1996)zbMATHCrossRefGoogle Scholar
  6. 6.
    Harel, D.: Statecharts: A visual formalism for complex systems. Science of Computer Programming 8, 231–274 (1987)zbMATHCrossRefMathSciNetGoogle Scholar
  7. 7.
    International Telecommunications Union (ITU): ITU-T Recommendation Z.100, Specification and Description Language (SDL) (2002), available at http://www.sdl-forum.org
  8. 8.
    Lamport, L.: The temporal logic of actions. ACM Transactions on Programming Languages and Systems 16 (1994)Google Scholar
  9. 9.
    Gurevich, M.: Evolving algebras 1993: Lipari guide. In: Börger, E. (ed.) Specification and Validation Methods, pp. 9–36. Oxford University Press, Oxford (1995)Google Scholar
  10. 10.
    Henzinger, T.: The theory of hybrid automata. In: Proceedings of the 11th LICS, pp. 278–292. IEEE Comp. Soc. Press, Los Alamitos (1996)Google Scholar
  11. 11.
    The Object Management Group (OMG): OMG Unified Modeling Language Specification Version 1.5 (2003) available at http://www.omg.org/technology/documents/formal/uml.htm
  12. 12.
    Bjørner, D., George, C.W., Haxthausen, A.E., Madsen, C.K., Holmslykke, S., Pěnička, M.: UML–ising” formal techniques. In: Ehrig, H., Damm, W., Desel, J., Große-Rhode, M., Reif, W., Schnieder, E., Westkämper, E. (eds.) INT 2004. LNCS, vol. 3147, pp. 423–450. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  13. 13.
    Kardos, M., Rammig, F.J.: Model based verification of distributed production control systems. In: Ehrig, H., Damm, W., Desel, J., Große-Rhode, M., Reif, W., Schnieder, E., Westkämper, E. (eds.) INT 2004. LNCS, vol. 3147, pp. 451–473. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  14. 14.
    Vesley, W., Dugan, J., Fragole, J., II, J.M., Railsback, J.: Fault Tree Handbook with Aerospace Applications. NASA Office of Safety and Mission Assurance, NASA Headquarters, Washington DC 20546 (2002) Google Scholar
  15. 15.
    Reifer, D.: Software failure modes and effects analysis. IEEE Transactions on Reliability 28, 147–249 (1979)CrossRefGoogle Scholar
  16. 16.
    Fenelon, P., McDermid, J., Nicholson, A., Pumfrey, D.: Experience with the application of HAZOP to computer-based systems. In: Proceedings of the 10th Annual Conference on Computer Assurance, Gaithersburg, MD, IEEE, Los Alamitos (1995)Google Scholar
  17. 17.
    Ortmeier, F., Thums, A., Schellhorn, G., Reif, W.: Combining formal methods and safety analysis - the for mossa approach. In: Ehrig, H., Damm, W., Desel, J., Große-Rhode, M., Reif, W., Schnieder, E., Westkämper, E. (eds.) INT 2004. LNCS, vol. 3147, pp. 474–493. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  18. 18.
    Brill, M., Buschermöhle, R., Damm, W., Klose, J., Westphal, B., Wittke, H.: Formal verification of LSCs in the development process. In: Ehrig, H., Damm, W., Desel, J., Große-Rhode, M., Reif, W., Schnieder, E., Westkämper, E. (eds.) INT 2004. LNCS, vol. 3147, pp. 494–516. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  19. 19.
    Paulson, L.C.: Isabelle: A Generic Theorem Prover. In: Paulson, L.C. (ed.) Isabelle. LNCS, vol. 828, Springer, Heidelberg (1994)CrossRefGoogle Scholar
  20. 20.
    Owre, S., Rushby, J.M., Shankar, N.: PVS: A Prototype Verification System. In: Kapur, D. (ed.) CADE 1992. LNCS (LNAI), vol. 607, Springer, Heidelberg (1992)Google Scholar
  21. 21.
    Kaufmann, M., Moore, J.: An industrial strength theorem prover for a logic based on common lisp. IEEE Transactions on Software Engineering 23 (1997)Google Scholar
  22. 22.
    Thums, A., Schellhorn, G., Ortmeier, F., Reif, W.: Interactive verification of statecharts. In: Ehrig, H., Damm, W., Desel, J., Große-Rhode, M., Reif, W., Schnieder, E., Westkämper, E. (eds.) INT 2004. LNCS, vol. 3147, pp. 355–373. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  23. 23.
    McMillan, K.L.: Symbolic Model Checking. Kluwer Academic Publishers, Dordrecht (1990)Google Scholar
  24. 24.
    Holzmann, G., Holzmann, G.: The Spin Model Checker: Primer and Reference Manual. Addison-Wesley, Reading (2003)Google Scholar
  25. 25.
    Amnell, T., Behrmann, G., Bengtsson, J., D’Argenio, P.R., David, A., Fehnker, A., Hune, T., Jeannet, B., Larsen, K.G., Möller, M.O., Pettersson, P., Weise, C., Yi, W.: Uppaal - Now, Next, and Future. In: Cassez, F., Jard, C., Rozoy, B., Dermot, M. (eds.) MOVEP 2000. LNCS, vol. 2067, pp. 100–125. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  26. 26.
    Bienmöller, T., Damm, W., Wittke, H.: The STATEMATE verification environment – making it real. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 561–567. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  27. 27.
    Bauer, N., Engell, S., Huuck, R., Lohmann, S., Lukoschus, B., Remelhe, M., Stursberg, O.: Verification of PLC programs given as sequential function charts. In: Ehrig, H., Damm, W., Desel, J., Große-Rhode, M., Reif, W., Schnieder, E., Westkämper, E. (eds.) INT 2004. LNCS, vol. 3147, pp. 517–540. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  28. 28.
    Ruf, J., Weiss, R.J., Kropf, T., Rosenstiel, W.: Modeling and formal verification of production automation systems. In: Ehrig, H., Damm, W., Desel, J., Große-Rhode, M., Reif, W., Schnieder, E., Westkämper, E. (eds.) INT 2004. LNCS, vol. 3147, pp. 541–566. Springer, Heidelberg (2004)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2004

Authors and Affiliations

  • Frank Ortmeier
    • 1
  • Wolfgang Reif
    • 1
  • Gerhard Schellhorn
    • 1
  1. 1.Lehrstuhl für Softwaretechnik und ProgrammiersprachenUniversität AugsburgAugsburg

Personalised recommendations