Model Checking: A Tutorial Overview - USF

← Back to document page

Model checking : A Tutorial OverviewStephan MerzInstitut f ur Informatik, Universit at M survey principles of Model checking techniques for the automaticanalysis of reactive systems. The use of Model checking is exemplified by ananalysis of the Needham-Schroeder public key protocol. We then formally de-fine transition systems, temporal logic, -automata, and their relationship. Basicmodel checking algorithms for linear- and branching-time temporal logics are de-fined, followed by an introduction to symbolic Model checking and partial-orderreduction techniques. The paper ends with a list of references to some more ad-vanced IntroductionComputerized systems pervade more and more our everyday lives.

Model Checking: A Tutorial Overview Stephan Merz Institut fur Informatik, Universit¨ ¨at M ¨unchen merz@informatik.uni-muenchen.de Abstract. We survey principles of model checking techniques for the automatic analysis of reactive systems. The use of model checking is exemplified by an

  Principles, Model, Overview, Tutorials, Checking, Principles of model checking, Model checking, A tutorial overview, Of model checking